nndist_inr

Mathlib.Analysis.Normed.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.nndist_inr

English

The nndist between inr a and inr b equals the nndist between a and b.

Русский

NNDist(inr a, inr b) = NNDist(a,b).

LaTeX

$$$$\\mathrm{nndist}((a: Unitization 𝕜 A),(b: Unitization 𝕜 A)) = \\mathrm{nndist}(a,b).$$$$

Lean4

theorem nndist_inr (a b : A) : nndist (a : Unitization 𝕜 A) (b : Unitization 𝕜 A) = nndist a b :=
  isometry_inr.nndist_eq a b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru