notMem_of_lt_csInf — Mathlib

English

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

Русский

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

LaTeX

$$$x < \mathrm{sInf}(s) \rightarrow BddBelow(s) \rightarrow x \notin s$$$

Lean4

theorem notMem_of_lt_csInf {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) : x ∉ s := fun hx =>
  lt_irrefl _ (h.trans_le (csInf_le hs hx))

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