lift — Mathlib

English

Lift a PosSMulMono structure from γ to β using a monotone embedding f and a smul-respecting map.

Русский

Переносим структуру PosSMulMono с γ на β с помощью монотонного вложения f и отображения, сохраняющего умножение скаляра.

LaTeX

$$$\text{PosSMulMono α β}$ via lift along f$$

Lean4

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

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