English
Assuming PosSMulStrictMono on γ and a suitable order-preserving map f: β → γ compatible with smul, PosSMulStrictMono on β is obtained by lifting from γ.
Русский
Предполагая PosSMulStrictMono на γ и подходящее отображение f: β → γ, совместимое с умножением, PosSMulStrictMono на β получается путем переноса со γ.
LaTeX
$$$\mathrm{PosSMulStrictMono} \;\alpha \;\beta$ via lift along f$$
Lean4
instance instSMulPosStrictMono [∀ i, SMulPosStrictMono α (β i)] : SMulPosStrictMono α (∀ i, β i) where
smul_lt_smul_of_pos_right := by
simp_rw [lt_def]
rintro a ⟨ha, i, hi⟩ _b₁ _b₂ hb
exact
⟨smul_le_smul_of_nonneg_right hb.le ha, i, smul_lt_smul_of_pos_right hb hi⟩
-- Note: There is no interesting instance for `PosSMulReflectLT α (∀ i, β i)` that's not already
-- implied by the other instances
