notMem_of_lt_csInf'

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#notMem_of_lt_csInf'

English

If x < sInf s, then x ∉ s.

Русский

Если x меньше sInf s, то x не принадлежит s.

LaTeX

$$$x < sInf(s) \Rightarrow x \notin s$$$

Lean4

theorem notMem_of_lt_csInf' {x : α} {s : Set α} (h : x < sInf s) : x ∉ s :=
  notMem_of_lt_csInf h (OrderBot.bddBelow s)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru