sInf_sup_le_iInf_sup

Mathlib.Order.CompleteLattice.Lemmas

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

← MathLib Explorer

English

For a in α and a set s ⊆ α, the inequality sup_{b∈s} (b ∧ a) ≤ sSup s ∧ a holds.

Русский

Для a и множества s ⊆ α верно: sup_{b∈s} (b ∧ a) ≤ sup s ∧ a.

LaTeX

$$$\displaystyle \sup_{b \in s} (b \wedge a) \le (\sup s) \wedge a$$$

Lean4

/-- This is a weaker version of `sInf_sup_eq` -/
theorem sInf_sup_le_iInf_sup : sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a :=
  le_iInf₂ fun _ h => sup_le_sup_right (sInf_le h) _

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

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

Разделы

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

Аффилиация

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