mk_eq_two_iff' — Mathlib

English

If |α| = 2, then for a fixed x there exists a unique y ≠ x such that the pair {x,y} enumerates α.

Русский

Если |α| = 2, то для заданного x существует единственный y ≠ x такое, что пара {x,y} задаёт весь набор.

LaTeX

$$$|\\alpha| = 2 \\Rightarrow \\exists! y, y \\neq x$$$

Lean4

theorem mk_eq_two_iff' (x : α) : #α = 2 ↔ ∃! y, y ≠ x :=
  by
  rw [mk_eq_two_iff]; constructor
  · rintro ⟨a, b, hne, h⟩
    simp only [eq_univ_iff_forall, mem_insert_iff, mem_singleton_iff] at h
    rcases h x with (rfl | rfl)
    exacts [⟨b, hne.symm, fun z => (h z).resolve_left⟩, ⟨a, hne, fun z => (h z).resolve_right⟩]
  · rintro ⟨y, hne, hy⟩
    exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

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