sSup_le — Mathlib

English

If every f ∈ c satisfies f ≤ g, then sSup c ≤ g.

Русский

Если каждый f ∈ c удовлетворяет f ≤ g, то sSup c ≤ g.

LaTeX

$$$$ \\forall f\\in c, f \\le g \\implies \\mathrm{sSup}(c) \\le g. $$$$

Lean4

protected theorem sSup_le {c : Set (E →ₗ.[R] F)} (hc : DirectedOn (· ≤ ·) c) {g : E →ₗ.[R] F} (hg : ∀ f ∈ c, f ≤ g) :
    LinearPMap.sSup c hc ≤ g :=
  le_of_eqLocus_ge <|
    sSup_le fun _ ⟨f, hf, Eq⟩ =>
      Eq ▸
        have : f ≤ LinearPMap.sSup c hc ⊓ g := le_inf (LinearPMap.le_sSup _ hf) (hg f hf)
        this.1

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