nnnorm_div_eq_nnnorm_left — Mathlib

English

For any x ∈ E and y ∈ E with ‖y‖₊ = 0, the NN-norm of x/y equals the NN-norm of x: ‖x/y‖₊ = ‖x‖₊.

Русский

Для любых x,y ∈ E при ‖y‖₊ = 0 имеем ‖x/y‖₊ = ‖x‖₊.

LaTeX

$$$$ \\|x / y\\|_{+} = \\|x\\|_{+} \\quad\\text{если } \\|y\\|_{+} = 0 $$$$

Lean4

@[to_additive]
theorem nnnorm_div_eq_nnnorm_left (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x / y‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_div_eq_norm_left _ <| congr_arg NNReal.toReal h

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