dual_solid — Mathlib

English

In a normed lattice-ordered group, if b ⊓ -b ≤ a ⊓ -a, then ∥a∥ ≤ ∥b∥.

Русский

В нормированной упорядоченной по lattice группе, если b ∧ (−b) ≤ a ∧ (−a), то ∥a∥ ≤ ∥b∥.

LaTeX

$$$b \wedge (-b) \le a \wedge (-a) \Rightarrow \|a\| \le \|b\|$$$

Lean4

theorem dual_solid (a b : α) (h : b ⊓ -b ≤ a ⊓ -a) : ‖a‖ ≤ ‖b‖ :=
  by
  apply solid
  rw [abs]
  nth_rw 1 [← neg_neg a]
  rw [← neg_inf]
  rw [abs]
  nth_rw 1 [← neg_neg b]
  rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]
    -- see Note [lower instance priority]

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