feat(Order/Interval/Finset/Box): add lemma (#12444)

Add `eq_zero_iff_eq_zero_of_mem_box` lemma needed for #10377
leanprover-community · May 16, 2024 · 01a8e4e · 01a8e4e
1 parent 1bf0efa
commit 01a8e4e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Order/Interval/Finset/Box.lean b/Mathlib/Order/Interval/Finset/Box.lean
@@ -48,6 +48,9 @@ lemma box_succ_disjUnion (n : ℕ) :
 
 @[simp] lemma zero_mem_box : (0 : α) ∈ box n ↔ n = 0 := by cases n <;> simp [box_succ_eq_sdiff]
 
+lemma eq_zero_iff_eq_zero_of_mem_box  {x : α} (hx : x ∈ box n) : x = 0 ↔ n = 0 :=
+  ⟨zero_mem_box.mp ∘ (· ▸ hx), fun hn ↦ by rwa [hn, box_zero, mem_singleton] at hx⟩
+
 end Finset
 
 open Finset