one_add_norm_le_sqrt_two_mul_sqrt

English

For every x in a normed additive group, 1 + ||x|| ≤ √2 √(1 + ||x||^2).

Русский

Для любого элемента x в нормированной аддитивной группе выполняется 1 + ||x|| ≤ √2 √(1 + ||x||^2).

LaTeX

$$$$1 + \|x\| \le \sqrt{2}\ \sqrt{1 + \|x\|^2}$$$$

Lean4

theorem one_add_norm_le_sqrt_two_mul_sqrt (x : E) : (1 : ℝ) + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2) :=
  by
  rw [← sqrt_mul zero_le_two]
  have := sq_nonneg (‖x‖ - 1)
  apply le_sqrt_of_sq_le
  linarith

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