subsingleton_setOf_mem_iff_pairwise_disjoint

English

A family f is pairwise disjoint iff for every a, the set { i : a ∈ f i } is a subsingleton.

Русский

Семейство f попарно непересекается тогда и только тогда, когда для каждого a множество { i : a ∈ f i } является одноэлементным (или пустым).

LaTeX

$$$$\big( \forall a, \{i \mid a \in f i\}.\text{Subsingleton} \big) \iff \text{PairwiseDisjoint } f.$$$$

Lean4

theorem subsingleton_setOf_mem_iff_pairwise_disjoint {f : ι → Set α} :
    (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f) :=
  ⟨fun h _ _ hij ↦ disjoint_left.2 fun a hi hj ↦ hij (h a hi hj), fun h _ _ hx _ hy ↦
    by_contra fun hne ↦ disjoint_left.1 (h hne) hx hy⟩

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