disjoint_sSup_left — Mathlib

English

If a is disjoint from the supremum of a directed family s, then the supremum of s is disjoint from a; equivalently, Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a.

Русский

Если sSup s не пересекается с a, то sSup s не пересекается с a; эквивалентно: Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a.

LaTeX

$$$ \mathrm{Disjoint}(\, \operatorname{sSup} s\, , a) \iff \forall b \in s, \mathrm{Disjoint}(b, a) $$$

Lean4

protected theorem disjoint_sSup_left (h : DirectedOn (· ≤ ·) s) : Disjoint (sSup s) a ↔ ∀ ⦃b⦄, b ∈ s → Disjoint b a :=
  by simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]

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