norm_map_of_map_one — Mathlib

English

There exists an index i with the property that either t is nonempty implies i ∈ t, and the product norm is bounded by ‖f(i)‖.

Русский

Существует индекс i так, что если t непусто, то i ∈ t, и нормa произведения ограничено ‖f(i)‖.

LaTeX

$$$\\exists i : ι,\\ (t.Nonempty \\rightarrow i \\in t) \\land \\left\\|\\prod_{j \\in t} f(j)\\right\\| \\le \\|f(i)\\|$$$

Lean4

@[to_additive]
theorem norm_map_of_map_one {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖ = ‖x‖ := by
  rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]

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