smul_iInf_le — Mathlib

English

For any m ∈ M and a function t: ι → α into a complete lattice α, m • iInf t ≤ ⨅ i, m • t(i).

Русский

Для любого m и функции t: ι → α в \\, α полную решётку, выполняется m • inf_i t ≤ inf_i (m • t(i)).

LaTeX

$$$ [SMul M α] [CompleteLattice α] [CovariantClass M α HSMul LE.le] {m : M} {t : ι → α} : m \\cdot \\inf t \\le \\inf_i (m \\cdot t i). $$$

Lean4

theorem smul_iInf_le [SMul M α] [CompleteLattice α] [CovariantClass M α HSMul.hSMul LE.le] {m : M} {t : ι → α} :
    m • iInf t ≤ ⨅ i, m • t i :=
  le_iInf fun _ => smul_mono_right _ (iInf_le _ _)

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