disjoint_sSup_iff — Mathlib

English

For any a and any set s, a is disjoint from sSup s if and only if a is disjoint from every member of s.

Русский

Для любых a и множества s: a несовместим с sSup s тогда и только тогда, когда a несовместим с каждым элементом s.

LaTeX

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

Lean4

theorem disjoint_sSup_iff {s : Set α} : Disjoint a (sSup s) ↔ ∀ b ∈ s, Disjoint a b := by
  simpa only [disjoint_comm] using @sSup_disjoint_iff

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