iSup_inf_le_sSup_inf — Mathlib

English

A variant of the previous statement describing how the infimum interacts with suprema inside an infimum over a set.

Русский

Вариант предыдущего утверждения о том, как инфиминум взаимодействует с верхними гранями внутри инфиминума по множеству.

LaTeX

$$$\displaystyle \text{(variant of iSup_inf_le_sSup_inf)}$$$

Lean4

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

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