eqv_classes_disjoint — Mathlib

English

If c is a set of pairwise disjoint blocks whose union is the whole α, then every element a ∈ α lies in a unique block of c.

Русский

Если множество блоков c попарно непересекается и их объединение даёт всё α, то каждый элемент a принадлежит ровно одному блоку c.

LaTeX

$$Let hu: c.sUnion = α and H: c.PairwiseDisjoint id; then ∀ a ∈ α, ∃! b ∈ c, a ∈ b.$$

Lean4

/-- Distinct elements of a set of sets partitioning α are disjoint. -/
theorem eqv_classes_disjoint {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) : c.PairwiseDisjoint id :=
  fun _b₁ h₁ _b₂ h₂ h =>
  Set.disjoint_left.2 fun x hx1 hx2 => (H x).elim fun _b _hc _hx => h <| eq_of_mem_eqv_class H h₁ hx1 h₂ hx2

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