norm_eq_of_mul_norm_lt_max

Mathlib.Analysis.Normed.Group.Ultra

URI: https://scilib.ai/kg/mathlib#IsUltrametricDist.norm_eq_of_mul_norm_lt_max

← MathLib Explorer

English

If ‖xy‖ < max(‖x‖, ‖y‖), then ‖x‖ = ‖y‖.

Русский

Если ‖xy‖ < max(‖x‖, ‖y‖), то ‖x‖ = ‖y‖.

LaTeX

$$$\\|xy\\| < \\max(\\|x\\|, \\|y\\|) \\Rightarrow \\|x\\| = \\|y\\|$$$

Lean4

@[to_additive]
theorem norm_eq_of_mul_norm_lt_max {x y : S} (h : ‖x * y‖ < max ‖x‖ ‖y‖) : ‖x‖ = ‖y‖ :=
  not_ne_iff.mp (h.ne ∘ norm_mul_eq_max_of_norm_ne_norm)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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