inner_lt_norm_mul_iff_real — Mathlib

English

For any x,y, ⟪x,y⟫ℝ < ∥x∥ ∥y∥ iff ⟪x,y⟫ is not maximal; equivalently ⟪x,y⟫ℝ < ∥x∥ ∥y∥ iff ‖y‖ x ≠ ‖x‖ y.

Русский

Для любых x,y: ⟪x,y⟫ℝ < ∥x∥ ∥y∥ тогда и только тогда, когда ‖y‖x ≠ ‖x‖y.

LaTeX

$$$⟪x,y⟫_{\mathbb{R}} < ∥x∥ ∥y∥ \iff ∥y∥ \cdot x \neq ∥x∥ \cdot y$$$

Lean4

theorem inner_lt_norm_mul_iff_real {x y : F} : ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y :=
  calc
    ⟪x, y⟫_ℝ < ‖x‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ ≠ ‖x‖ * ‖y‖ := ⟨ne_of_lt, lt_of_le_of_ne (real_inner_le_norm _ _)⟩
    _ ↔ ‖y‖ • x ≠ ‖x‖ • y := not_congr inner_eq_norm_mul_iff_real

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