disjoint_sSup_right — Mathlib

English

If a set of elements is disjoint from b, then b is disjoint from any element of the set a.

Русский

Если множество a элементов несовместно с b, то b несовместен с любым элементом множества a.

LaTeX

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

Lean4

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

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