disjoint_sSup_left — Mathlib

English

If a is a set and b ∈ α with the property that a is disjoint from b, then any element i of a is also disjoint from b.

Русский

Если множество a и элемент b удовлетворяют условию взаимного непересечения, то любой элемент i из a также не пересекается с b.

LaTeX

$$$\forall i \in a,\; \operatorname{Disjoint}(i,b)$$$

Lean4

theorem disjoint_sSup_left {a : Set α} {b : α} (d : Disjoint (sSup a) b) {i} (hi : i ∈ a) : Disjoint i b :=
  disjoint_iff_inf_le.mpr (iSup₂_le_iff.1 (iSup_inf_le_sSup_inf.trans d.le_bot) i hi :)

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