disjoint_of_sSup_disjoint — Mathlib

English

If the supremum of a family a is disjoint from b, then a and b are disjoint provided a and b do not contain bottom as an element.

Русский

Если верхняя граница множества a не пересекается с b, то a и b несовместны при условии, что они не содержат нуль как элемент.

LaTeX

$$$\forall a,b\; Disjoint (sSup a) (sSup b) \Rightarrow (Not (b \in a) \lor Not (b \in b))$$$

Lean4

theorem disjoint_of_sSup_disjoint {a b : Set α} (hd : Disjoint (sSup a) (sSup b)) (he : ⊥ ∉ a ∨ ⊥ ∉ b) : Disjoint a b :=
  disjoint_of_sSup_disjoint_of_le_of_le (fun _ hc ↦ le_sSup hc) (fun _ hc ↦ le_sSup hc) hd he

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