instSMulPosReflectLE — Mathlib

English

If every β_i has PosSMulPosLTReflect, then the Pi-type ∀ i, β_i inherits PosSMulPosReflectLT, i.e., a nonnegative scalar preserves strict inequality componentwise.

Русский

Если каждый β_i имеет PosSMulPosLTReflect, то Π-тип ∀ i, β_i наследует PosSMulPosReflectLT, то есть неотрицательный скаляр сохраняет строгую неравенство по компонентам.

LaTeX

$$$\text{PosSMulPosReflectLT} \;((i) \mapsto β_i)$$$

Lean4

instance instSMulPosReflectLE [∀ i, SMulPosReflectLE α (β i)] : SMulPosReflectLE α (∀ i, β i) where
  le_of_smul_le_smul_right _b hb _a₁ _a₂
    h := by obtain ⟨-, i, hi⟩ := lt_def.1 hb; exact le_of_smul_le_smul_right (h _) hi

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