norm_eq_of_norm_add_lt_right

Mathlib.NumberTheory.Padics.PadicNumbers

URI: https://scilib.ai/kg/mathlib#Padic.norm_eq_of_norm_add_lt_right

← MathLib Explorer

English

If ‖z1 + z2‖_p < ‖z2‖_p, then ‖z1‖_p = ‖z2‖_p.

Русский

Если ‖z1 + z2‖_p < ‖z2‖_p, тогда ‖z1‖_p = ‖z2‖_p.

LaTeX

$$$‖z_1 + z_2‖_p < ‖z_2‖_p \\Rightarrow ‖z_1‖_p = ‖z_2‖_p$$$

Lean4

theorem norm_eq_of_norm_add_lt_right {z1 z2 : ℚ_[p]} (h : ‖z1 + z2‖ < ‖z2‖) : ‖z1‖ = ‖z2‖ :=
  _root_.by_contradiction fun hne ↦ not_lt_of_ge (by rw [add_eq_max_of_ne hne]; apply le_max_right) h

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

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

Разделы

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

Аффилиация

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