toIsStrictOrderedModule — Mathlib

English

For any real-valued scalars, the action of ℝ on K respects strict order: if r > 0 and x < y then r·x < r·y, and similarly on the right.

Русский

Действие вещественных чисел на K сохраняет строгий порядок: если r > 0 и x < y тогда r·x < r·y, а также слева и справа.

LaTeX

$$$IsStrictOrderedModule(\mathbb{R}, K)$$$

Lean4

theorem toIsStrictOrderedModule : IsStrictOrderedModule ℝ K
    where
  smul_lt_smul_of_pos_left r hr a b
    hab := by simpa [RCLike.lt_iff_re_im (K := K), smul_re, smul_im, hr, hr.ne'] using hab
  smul_lt_smul_of_pos_right a ha r₁ r₂
    hr := by
    obtain ⟨hare, haim⟩ := RCLike.lt_iff_re_im.1 ha
    simp_all [RCLike.lt_iff_re_im (K := K), smul_re, smul_im]

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