sSup_le_sSup_of_subset_insert_bot

Mathlib.Order.CompleteLattice.Basic

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

English

If s is contained in insert ⊥ t, then sSup s ≤ sSup t.

Русский

Если s ⊆ insert ⊥ t, то sSup s ≤ sSup t.

LaTeX

$$$$ s \subseteq \operatorname{insert} (\bot) t \Rightarrow \operatorname{sSup}(s) \le \operatorname{sSup}(t) $$$$

Lean4

theorem sSup_le_sSup_of_subset_insert_bot (h : s ⊆ insert ⊥ t) : sSup s ≤ sSup t :=
  (sSup_le_sSup h).trans_eq (sSup_insert.trans (bot_sup_eq _))

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

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

Разделы

Аффилиация

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