iSup_disjoint_iff — Mathlib

English

Disjointness with a supremum is equivalent to disjointness with each component: Disjoint (⨆ i, f i) a ⇔ ∀ i, Disjoint (f i) a.

Русский

Свойство несовместности с sup эквивалентно несовместности с каждой компонентой: Disjoint (⨆ i, f i) a ⇔ ∀ i, Disjoint (f i) a.

LaTeX

$$$\\operatorname{Disjoint}\\Bigl( \\bigvee_i f(i), a \\Bigr) \\quad\\Leftrightarrow\\quad \\forall i, \\operatorname{Disjoint}(f(i), a)$$$

Lean4

theorem iSup_disjoint_iff {f : ι → α} : Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a := by
  simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]

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