pairwiseDisjoint_fiber — Mathlib

English

For any function f: ι → α and any subset s ⊆ α, the fiber sets f⁻¹({a}) for different a ∈ α are pairwise disjoint.

Русский

Для любой функции f: ι → α и любой подмножества s ⊆ α множество ответов фибр f⁻¹({a}) различны для разных a ∈ α; эти множества попарно непересекаются.

LaTeX

$$$$\text{For } f: \iota \to \alpha, \ s \subseteq \alpha: \ s.\ PairwiseDisjoint (\\xrightarrow{f} \{a\}) \\Longleftrightarrow \ \forall a,b \in s, a \neq b \Rightarrow f^{-1}\\{a\\} \cap f^{-1}\\{b\\} = \emptyset.$$$$

Lean4

theorem pairwiseDisjoint_fiber (f : ι → α) (s : Set α) : s.PairwiseDisjoint fun a => f ⁻¹' { a } := fun _a _ _b _ h =>
  disjoint_iff_inf_le.mpr fun _i ⟨hia, hib⟩ => h <| (Eq.symm hia).trans hib

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