enorm_eq_enorm' — Mathlib

English

If u and v are inseparable, their enorms are equal: ‖u‖ₑ = ‖v‖ₑ.

Русский

Если u и v неразделимы, то их enorm равны: ‖u‖ₑ = ‖v‖ₑ.

LaTeX

$$$ \text{Inseparable}(u,v) \Rightarrow \|u\|_e = \|v\|_e. $$$

Lean4

@[to_additive Inseparable.enorm_eq_enorm]
theorem enorm_eq_enorm' {E : Type*} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) :
    ‖u‖ₑ = ‖v‖ₑ :=
  h.map continuous_enorm |>.eq

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