lift — Mathlib

English

Lift a PosSMulReflectLT structure along a monotone map f; nonnegative smul preserves strict inequalities componentwise.

Русский

Переносим PosSMulReflectLT вдоль монотонного отображения f; неотрицательное скалярное умножение сохраняет строгие неравенства по компонентам.

LaTeX

$$$\text{PosSMulReflectLT α β}$ via lift$$

Lean4

theorem lift [PosSMulReflectLT α γ] (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) b, f (a • b) = a • f b) :
    PosSMulReflectLT α β where
  lt_of_smul_lt_smul_left a ha b₁ b₂
    h := by simp only [← lt_iff_lt_of_le_iff_le' hf hf, smul] at *; exact lt_of_smul_lt_smul_left h ha

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