instPosSMulStrictMono — Mathlib

English

If every β_i has PosSMulStrictMono, then the Pi-type ∀ i, β_i inherits PosSMulStrictMono; a strictly positive scalar preserves strict inequality componentwise.

Русский

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

LaTeX

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

Lean4

instance instPosSMulStrictMono [∀ i, PosSMulStrictMono α (β i)] : PosSMulStrictMono α (∀ i, β i) where
  smul_lt_smul_of_pos_left := by
    simp_rw [lt_def]
    rintro _a ha _b₁ _b₂ ⟨hb, i, hi⟩
    exact ⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩

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