pairwiseDisjoint_range_singleton — Mathlib

English

The family of all singletons {i} in ι, viewed as subsets of ι, is pairwise disjoint.

Русский

Семейство всех множеств-одиночек {i} в ι, как подмножества ι, попарно не пересекается.

LaTeX

$$$$\big\{\{i\}: i \in \iota\big\} \text{ состоит из попарно непересекающихся множеств, т. е. } (\{i\}\cap\{j\})=\emptyset \text{ для } i\neq j.$$$$

Lean4

theorem pairwiseDisjoint_range_singleton : (range (singleton : ι → Set ι)).PairwiseDisjoint id :=
  Pairwise.range_pairwise fun _ _ => disjoint_singleton.2

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