le_iff_oneLePart_leOnePart — Mathlib

English

For all a,b in the lattice-ordered group with left-mono, the order relation is characterized by the parts: a ≤ b iff a⁺ᵐ ≤ b⁺ᵐ and b⁻ᵐ ≤ a⁻ᵐ.

Русский

Для любых a,b в упорядоченной группе с монотонностью слева: a ≤ b тогда и только тогда, когда a⁺ᵐ ≤ b⁺ᵐ и b⁻ᵐ ≤ a⁻ᵐ.

LaTeX

$$$a \le b \iff a^{+m} \le b^{+m} \land b^{-m} \le a^{-m}$$$

Lean4

@[to_additive]
theorem le_iff_oneLePart_leOnePart (a b : α) : a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ :=
  by
  refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩
  rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b]
  exact div_le_div'' h.1 h.2

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