erase_nonempty — Mathlib

English

If a ∈ s and a ∉ t, then erase s a = t if and only if s = insert a t.

Русский

Если a ∈ s и a ∉ t, то erase s a = t тогда и только тогда, когда s = insert a t.

LaTeX

$$$$ \text{erase } s a = t \iff s = \text{insert } a\ t \quad \text{given } a \in s, a \notin t. $$$$

Lean4

@[simp]
theorem erase_nonempty (ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial :=
  by
  simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]
  refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
  rintro ⟨b, hb, hba⟩
  exact ⟨_, hb, _, ha, hba⟩

Похожие утверждения