lift — Mathlib

English

Lift a SMulPosReflectLT structure along a map preserving order; nonnegative smul preserves strict inequalities.

Русский

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

LaTeX

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

Lean4

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

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