lift — Mathlib

English

Lift a SMulPosMono structure along a map that preserves the zero and smul; the resulting β inherits SMulPosMono.

Русский

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

LaTeX

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

Lean4

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

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