disjoint_iSup_right — Mathlib

English

For a directed family f, a is disjoint from the join of all f(i) iff a is disjoint from each f(i): Disjoint a (iSup f i) ↔ ∀ i, Disjoint a (f i).

Русский

Для направленной семействa f: Disjoint a (iSup f) ⇔ ∀ i, Disjoint a (f i).

LaTeX

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

Lean4

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

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