pairwiseDisjoint_range_singleton — Mathlib

English

The family of singletons generated by the range of the singleton function is pairwise disjoint: {range singleton}.PairwiseDisjoint id.

Русский

Семейство одноэлементных интервалов порожденное последовательностью одиночек на множестве типов пар является попарно непересекающимся.

LaTeX

$$({\text{Set.range }}(\text{singleton} : α → Finset α)).PairwiseDisjoint id$$

Lean4

theorem pairwiseDisjoint_range_singleton : (Set.range (singleton : α → Finset α)).PairwiseDisjoint id :=
  by
  rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
  exact disjoint_singleton.2 (ne_of_apply_ne _ h)

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