eq_of_mem_eqv_class — Mathlib

English

If a point x belongs to two blocks b and b' in a partition c, then those two blocks are identical. More precisely, if b ∈ c, b' ∈ c, x ∈ b, and x ∈ b', then b = b'.

Русский

Если точка x принадлежит двум блокам b и b' внутри разбиения c, то эти блоки совпадают: b = b'.

LaTeX

$$$\\forall x, \\forall b,b' \\in c,\\ x \\in b \\land x \\in b' \\Rightarrow b = b'.$$$

Lean4

/-- If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal. -/
theorem eq_of_mem_eqv_class {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {x b b'} (hc : b ∈ c) (hb : x ∈ b)
    (hc' : b' ∈ c) (hb' : x ∈ b') : b = b' :=
  (H x).unique ⟨hc, hb⟩ ⟨hc', hb'⟩

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