pairwise_disjoint_fiber — Mathlib

English

For a function f: ι → Set α and s = univ, the family { f⁻¹' {a} : a ∈ α } is pairwise disjoint.

Русский

Для функции f: ι → Set α и s = всё множество α, семейство { f⁻¹' {a} : a ∈ α } попарно непересекается.

LaTeX

$$$$\text{pairwiseDisjoint } (\lambda a, f^{-1}\{a\})\; (\text{over } a \in \alpha).$$$$

Lean4

theorem pairwise_disjoint_fiber (f : ι → α) : Pairwise (Disjoint on fun a : α => f ⁻¹' { a }) :=
  pairwise_univ.1 <| Set.pairwiseDisjoint_fiber f univ

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