mk_eq_one_iff

Mathlib.Analysis.Normed.Group.Uniform

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.mk_eq_one_iff

English

For any p ∈ E, mk p = 1 in SeparationQuotient iff ‖p‖ = 0.

Русский

Для любого p ∈ E, mk p = 1 в SeparationQuotient тогда и только тогда, когда ‖p‖ = 0.

LaTeX

$$$\\mathrm{mk}\\,p = 1 \\iff \\|p\\| = 0$$$

Lean4

@[to_additive]
theorem mk_eq_one_iff {p : E} : mk p = 1 ↔ ‖p‖ = 0 := by rw [← norm_mk', norm_eq_zero']

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

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

Разделы

Аффилиация

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