norm_eq_of_nonempty — Mathlib

English

If α is nonempty, the same norm equals the infimum formula without the 0 ≤ C bound: ‖f‖ = sInf {C ∈ ℝ | ∀ x, ‖f(x)‖ ≤ C}.

Русский

Если множество α непусто, тогда норма равна инфимуму без условия 0 ≤ C: ‖f‖ = sInf {C ∈ ℝ | ∀ x, ‖f(x)‖ ≤ C}.

LaTeX

$$$‖f‖ = sInf\\{C ∈ \\mathbb{R} \\mid ∀ x, ‖f(x)‖ ≤ C\\}$$$

Lean4

/-- When the domain is non-empty, we do not need the `0 ≤ C` condition in the formula for `‖f‖` as a
`sInf`. -/
theorem norm_eq_of_nonempty [h : Nonempty α] : ‖f‖ = sInf {C : ℝ | ∀ x : α, ‖f x‖ ≤ C} :=
  by
  obtain ⟨a⟩ := h
  rw [norm_eq]
  congr
  ext
  simp only [and_iff_right_iff_imp]
  exact fun h' => le_trans (norm_nonneg (f a)) (h' a)

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