lift — Mathlib

English

Lift a SMulPosReflectLE structure along a map that preserves order; the input β inherits PosSMulReflectLE via smul.

Русский

Переносим SMulPosReflectLE вдоль отображения, сохраняющего порядок; β наследует PosSMulReflectLE через умножение скаляром.

LaTeX

$$$\text{SMulPosReflectLE α γ}$ via lift$$

Lean4

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

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