sup_sInf_le_iInf_sup — Mathlib

English

This gives a weaker version of a standard equality relating suprema and infima: a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b.

Русский

Это слабее стандартного равенства между сверху и снизу: a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b.

LaTeX

$$$a \lor \operatorname{sInf}(s) \leq \bigl( \bigwedge_{b \in s} (a \lor b) \bigr)$$$

Lean4

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

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