eq_insert_of_subset_of_encard_eq_succ

English

encard(s) ≤ 1 is equivalent to s being empty or a singleton.

Русский

encard(S) ≤ 1 эквивалентно тому, что S пусто или одноэлементно.

LaTeX

$$$encard(s) ≤ 1 \\iff s = \\emptyset \\lor \\exists x, s = { x }$$$

Lean4

theorem eq_insert_of_subset_of_encard_eq_succ (hs : s.Finite) (h : s ⊆ t) (hst : t.encard = s.encard + 1) :
    ∃ a, t = insert a s :=
  by
  rw [← encard_diff_add_encard_of_subset h, add_comm, WithTop.add_left_inj hs.encard_lt_top.ne, encard_eq_one] at hst
  obtain ⟨x, hx⟩ := hst; use x; rw [← diff_union_of_subset h, hx, singleton_union]

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