notMem_of_csSup_lt — Mathlib

English

If sSup(s) < x in a ConditionallyCompleteLattice, and s is bounded above, then x ∉ s.

Русский

Если sSup(s) < x в условной полноупорядоченной решётке и s ограничено сверху, то x не принадлежит s.

LaTeX

$$$\mathrm{sSup}(s) < x \rightarrow BddAbove(s) \rightarrow x \notin s$$$

Lean4

theorem notMem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) : x ∉ s :=
  notMem_of_lt_csInf (α := αᵒᵈ) h hs

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