le_iff_norm_sqrt_mul_sqrt_inv — Mathlib

English

For a≥0 and b unit, a ≤ b if and only if ‖sqrt(a) · sqrt(b^(-1))‖ ≤ 1, providing an alternative expression of the order.

Русский

Пусть a≥0 и b единица. Тогда a ≤ b тогда и только тогда, когда ‖sqrt(a) · sqrt(b^(-1))‖ ≤ 1, что даёт альтернативное выражение порядка.

LaTeX

$$a ≤ b \\iff \\|\\sqrt a \\cdot \\sqrt{\\!\\uparrow b^{-1}\\!} \\| ≤ 1$$

Lean4

theorem le_iff_norm_sqrt_mul_sqrt_inv {a : A} {b : Aˣ} (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
    a ≤ b ↔ ‖sqrt a * sqrt (↑b⁻¹ : A)‖ ≤ 1 :=
  by
  rw [CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)), ← CFC.rpow_neg_one_eq_inv b, CFC.rpow_rpow (b : A) _ _ (by simp) (by simp),
    le_iff_norm_sqrt_mul_rpow b.isUnit ha hb]
  simp

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