sSup_disjoint_iff — Mathlib

English

Let s be a set of elements of α. The element a is disjoint from the supremum of s if and only if every element of s is disjoint from a.

Русский

Пусть s — множество элементов α. Элемент a дисjointен с верхним пределом s тогда и только тогда, когда каждый элемент из s несовместен с a.

LaTeX

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

Lean4

theorem sSup_disjoint_iff {s : Set α} : Disjoint (sSup s) a ↔ ∀ b ∈ s, Disjoint b a := by
  simp only [disjoint_iff, sSup_inf_eq, iSup_eq_bot]

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