sInf_le_sInf_of_subset_insert_top

Mathlib.Order.CompleteLattice.Basic

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

← MathLib Explorer

English

If s ⊆ insert ⊤ t, then sInf t ≤ sInf s.

Русский

Если s ⊆ insert ⊤ t, то sInf t ≤ sInf s.

LaTeX

$$$$ s \subseteq \operatorname{insert} (\top) t \Rightarrow \operatorname{sInf}(t) \le \operatorname{sInf}(s) $$$$

Lean4

theorem sInf_le_sInf_of_subset_insert_top (h : s ⊆ insert ⊤ t) : sInf t ≤ sInf s :=
  (sInf_le_sInf h).trans_eq' (sInf_insert.trans (top_inf_eq _)).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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