csInf_eq_bot_of_bot_mem

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csInf_eq_bot_of_bot_mem

English

If ⊥ belongs to a set s in an OrderBot lattice, then sInf s = ⊥.

Русский

Если ⊥ принадлежит множеству s в порядке с нулём, то sInf s = ⊥.

LaTeX

$$$ (\bot \in s) \Rightarrow sInf s = \bot $$$

Lean4

theorem csInf_eq_bot_of_bot_mem [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥ :=
  eq_bot_iff.2 <| csInf_le (OrderBot.bddBelow s) hs

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

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

Разделы

Аффилиация

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