disjoint_iSup_iff — Mathlib

English

Simplified form: iSup_disjoint_iff states the same equivalence under a minimal axiom framework.

Русский

Упрощенная форма: iSup_disjoint_iff выражает эквивалентность подмножества несовместности.

LaTeX

$$$\\text{Disjoint}( \\bigvee_i f(i), a) \\iff \\forall i, \\text{Disjoint}(f(i), a)$$$

Lean4

theorem disjoint_iSup_iff {f : ι → α} : Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i) := by
  simpa only [disjoint_comm] using @iSup_disjoint_iff

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