toPosMulReflectLT — Mathlib

English

In a RCLike setting, left multiplication by a positive element is strictly order-preserving: if x < y, then a·x < a·y for all a > 0.

Русский

В рамках RCLike умножение слева на положительный элемент сохраняет порядок строго: если x < y, то a·x < a·y при любом a > 0.

LaTeX

$$$\forall a>0,\; x

Lean4

theorem toPosMulReflectLT : PosMulReflectLT K where
  elim := by
    rintro ⟨x, hx⟩ y z hyz
    dsimp at *
    rw [RCLike.le_iff_re_im, map_zero, map_zero, eq_comm] at hx
    obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2
    simp only [RCLike.lt_iff_re_im (K := K), mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero, mul_im, add_zero,
      mul_eq_mul_left_iff] at hyz ⊢
    refine ⟨lt_of_mul_lt_mul_of_nonneg_left hyz.1 <| by simpa using hx, hyz.2.resolve_right ?_⟩
    rintro rfl
    simp at hyz

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