pairwiseDisjoint — Mathlib

English

The sets in the partition are pairwise disjoint; i.e., for any A,B ∈ c with A ≠ B, A ∩ B = ∅.

Русский

Множества внутри разбиения попарно непересекаются; то есть для любых A,B ∈ c с A ≠ B выполняется A ∩ B = ∅.

LaTeX

$$$\\forall A,B \\in c,\\ A \\neq B \\Rightarrow A \\cap B = \\emptyset$$$

Lean4

theorem pairwiseDisjoint {c : Set (Set α)} (hc : IsPartition c) : c.PairwiseDisjoint id :=
  eqv_classes_disjoint hc.2

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