norm_eq_of_norm_add_lt_left

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.norm_eq_of_norm_add_lt_left

← MathLib Explorer

English

Symmetrically, if ||z1 + z2|| < ||z1||, then ||z1|| = ||z2||.

Русский

Аналогично, если ||z1 + z2|| < ||z1||, то ||z1|| = ||z2||.

LaTeX

$$$$\|z_1 + z_2\| < \|z_1\| \Rightarrow \|z_1\| = \|z_2\|.$$$$

Lean4

theorem norm_eq_of_norm_add_lt_left {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖ :=
  by_contra fun hne => not_lt_of_ge (by rw [norm_add_eq_max_of_ne hne]; apply le_max_left) h

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

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

Разделы

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

Аффилиация

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