norm_le_half_period — Mathlib

English

Let p be a nonzero real number. Then every element x of the additive circle AddCircle(p) satisfies the inequality ‖x‖ ≤ |p|/2.

Русский

Пусть p — ненулевое вещественное число. Тогда каждый элемент x аддитивного круга AddCircle(p) удовлетворяет неравенству ‖x‖ ≤ |p|/2.

LaTeX

$$$p \neq 0 \\Rightarrow \\forall x : \\mathrm{AddCircle}(p), \\; \\|x\\| \\le \\dfrac{|p|}{2}$$$

Lean4

theorem norm_le_half_period {x : AddCircle p} (hp : p ≠ 0) : ‖x‖ ≤ |p| / 2 :=
  by
  obtain ⟨x⟩ := x
  change ‖(x : AddCircle p)‖ ≤ |p| / 2
  rw [norm_eq, ← mul_le_mul_iff_right₀ (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub, mul_left_comm, ←
    mul_div_assoc, ← abs_mul, inv_mul_cancel₀ hp, mul_one, abs_one]
  exact abs_sub_round (p⁻¹ * x)

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