lift — Mathlib

English

Lift a PosSMulReflectLE structure along a monotone map f that preserves order; the induced β retains the reflection of ≤ via smul.

Русский

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

LaTeX

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

Lean4

theorem lift [PosSMulReflectLE α γ] (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) (smul : ∀ (a : α) b, f (a • b) = a • f b) :
    PosSMulReflectLE α β where
  le_of_smul_le_smul_left a ha b₁ b₂ h := hf.1 <| le_of_smul_le_smul_left (by simpa only [smul] using hf.2 h) ha

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