instSup — Mathlib

English

The space α →ᵇ γ is an algebra over 𝕜 with the structure map given by the constant algebra map and the pointwise operations.

Русский

Пространство α →ᵇ γ является алгеброй над 𝕜 со структурной картой константной алгебры и покоординатными операциями.

LaTeX

$$$\\text{Algebra}_{𝕜}(α \\to^b γ)$$$

Lean4

instance instSup : Max (α →ᵇ β) where
  max f
    g :=
    { toFun := f ⊔ g
      continuous_toFun := f.continuous.sup g.continuous
      map_bounded' := by
        obtain ⟨C₁, hf⟩ := f.bounded
        obtain ⟨C₂, hg⟩ := g.bounded
        refine ⟨C₁ + C₂, fun x y ↦ ?_⟩
        simp_rw [dist_eq_norm_sub] at hf hg ⊢
        exact (norm_sup_sub_sup_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _)) }

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