iSup_inf_le_inf_sSup

Mathlib.Order.CompleteLattice.Lemmas

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

English

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

Русский

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

LaTeX

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

Lean4

/-- This is a weaker version of `inf_sSup_eq` -/
theorem iSup_inf_le_inf_sSup : ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s :=
  @sup_sInf_le_iInf_sup αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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