disjoint_iSup_left — Mathlib

English

Symmetric statement: Disjoint (iSup f) a ↔ ∀ i, Disjoint (f i) a.

Русский

Симметрическое утверждение: Disjoint (iSup f) a ⇔ ∀ i, Disjoint (f i) a.

LaTeX

$$$ \mathrm{Disjoint}\left(\big\vee_i f(i), a\right) \iff \forall i, \mathrm{Disjoint}(f(i), a) $$$

Lean4

protected theorem disjoint_iSup_left (h : Directed (· ≤ ·) f) : Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a := by
  simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

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