sInf_diff_singleton_top

Mathlib.Order.CompleteLattice.Basic

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

English

Let α be a complete lattice. For any set s ⊆ α, removing the top element does not change its infimum: sInf(s \ {⊤}) = sInf(s).

Русский

Пусть α — полная решётка. Тогда sInf(s \ {⊤}) = sInf(s).

LaTeX

$$$$ \operatorname{sInf}(s \setminus \{ \top \}) = \operatorname{sInf}(s) $$$$

Lean4

@[simp]
theorem sInf_diff_singleton_top (s : Set α) : sInf (s \ {⊤}) = sInf s :=
  @sSup_diff_singleton_bot αᵒᵈ _ s

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

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

Разделы

Аффилиация

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