instInf — Mathlib

English

The space α →ᵇ β is equipped with a semilattice supremum operation, defined pointwise using the supremum in β.

Русский

У пространства α →ᵇ β задана операция наибольшего верхнего предела в виде покоординатного взятия supremum в β.

LaTeX

$$$f \\sqcup g$ defined by $(f \\sqcup g)(x) = f(x) \\sqcup g(x)$$$

Lean4

instance instInf : Min (α →ᵇ β) where
  min f
    g :=
    { toFun := f ⊓ g
      continuous_toFun := f.continuous.inf 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_inf_sub_inf_le_add_norm _ _ _ _).trans (add_le_add (hf _ _) (hg _ _)) }

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