exists_eq_insert_iff — Mathlib

English

There exists an element a not in s such that inserting a into s yields t iff s ⊆ t and |s| + 1 = |t|.

Русский

Существует элемент a, не входящий в s, такой что вставка a в s даёт t тогда и только тогда, когда s ⊆ t и |s| + 1 = |t|.

LaTeX

$$$(\\exists a \\notin s, \\text{ insert } a s = t) \\iff (s \\subseteq t \\land |s| + 1 = |t|)$$$

Lean4

theorem exists_eq_insert_iff [DecidableEq α] {s t : Finset α} : (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t :=
  by
  constructor
  · grind
  · rintro ⟨hst, h⟩
    obtain ⟨a, ha⟩ : ∃ a, t \ s = { a } := card_eq_one.mp (by grind)
    exact
      ⟨a, fun hs => (by grind : a ∉ { a }) <| mem_singleton_self _, by rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩

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