lift — Mathlib

English

Lift a PosSMulStrictMono structure along a order-preserving map; the resulting β inherits strict monotonicity under scalar action.

Русский

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

LaTeX

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

Lean4

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

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