edist_one_eq_enorm

Mathlib.Analysis.Normed.Group.Basic

URI: https://scilib.ai/kg/mathlib#edist_one_eq_enorm

English

Another formulation: edist x 1 equals the EN-norm of x; equivalently the distance to the identity matches the norm.

Русский

Еще одно выражение: edist x 1 = ‖x‖ₑ; расстояние к единице совпадает с нормой.

LaTeX

$$$$ \\mathrm{edist}(x,1) = \\|x\\|_{e} $$$$

Lean4

@[to_additive]
theorem edist_one_eq_enorm (x : E) : edist x 1 = ‖x‖ₑ := by rw [edist_eq_enorm_div, div_one]

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

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

Разделы

Аффилиация

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