csSup_le_csSup'

Mathlib.Order.ConditionallyCompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#csSup_le_csSup'

← MathLib Explorer

English

If BddAbove t and s ⊆ t, then sSup s ≤ sSup t.

Русский

Если t ограничено сверху и s ⊆ t, то sSup s ≤ sSup t.

LaTeX

$$$BddAbove(t) \Rightarrow sSup(s) \le sSup(t)$$$

Lean4

@[gcongr mid]
theorem csSup_le_csSup' {s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) : sSup s ≤ sSup t :=
  by
  rcases eq_empty_or_nonempty s with rfl | h
  · rw [csSup_empty]
    exact bot_le
  · exact csSup_le_csSup h₁ h h₂

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

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

Разделы

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

Аффилиация

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