norm_liftNormedAddGroupHom_apply_le

English

For a NormedAddGroupHom f and hf as above, the lifted map satisfies a pointwise bound: for all x in SeparationQuotient M, ||liftNormedAddGroupHom f hf x|| ≤ ||f|| · ||x||.

Русский

Для нормированного гомо-морфизма f и hf, подъемное отображение удовлетворяет локальной границе: для всех x ∈ SeparationQuotient M, ||liftNormedAddGroupHom f hf x|| ≤ ||f|| · ||x||.

LaTeX

$$$\\|\\mathrm{liftNormedAddGroupHom} f\\, hf\, x\\| \\leq \\|f\\| \\cdot \\|x\\|$$$

Lean4

theorem norm_liftNormedAddGroupHom_apply_le (f : NormedAddGroupHom M N) (hf : ∀ x, ‖x‖ = 0 → f x = 0)
    (x : SeparationQuotient M) : ‖liftNormedAddGroupHom f hf x‖ ≤ ‖f‖ * ‖x‖ :=
  by
  obtain ⟨x, rfl⟩ := surjective_mk x
  exact le_opNorm f x

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