eq_singleton_top_of_sInf_eq_top_of_nonempty

Mathlib.Order.CompleteLattice.Basic

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

English

If sInf s = ⊤ and s is nonempty, then s = {⊤}.

Русский

Если sInf s = ⊤ и s непусто, то s = {⊤}.

LaTeX

$$$$ sInf s = \top \Rightarrow s \text{ Nonempty } \Rightarrow s = \{ \top \} $$$$

Lean4

theorem eq_singleton_top_of_sInf_eq_top_of_nonempty : sInf s = ⊤ → s.Nonempty → s = {⊤} :=
  @eq_singleton_bot_of_sSup_eq_bot_of_nonempty αᵒᵈ _ _

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

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

Разделы

Аффилиация

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