smul_inf_le — Mathlib

English

For any m ∈ M and a1, a2 ∈ α in a lattice with CovariantClass, we have m • (a1 ⊓ a2) ≤ (m • a1) ⊓ (m • a2).

Русский

Для любого m и элементов a1, a2 области лейтовой структуры выполняется неравенство: m • (a1 ∧ a2) ≤ (m • a1) ∧ (m • a2).

LaTeX

$$$ [SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul LE.le] (m : M) (a_1 a_2 : α) : m • (a_1 \\inf a_2) \\le (m • a_1) \\inf (m • a_2). $$$

Lean4

theorem smul_inf_le [SMul M α] [SemilatticeInf α] [CovariantClass M α HSMul.hSMul LE.le] (m : M) (a₁ a₂ : α) :
    m • (a₁ ⊓ a₂) ≤ m • a₁ ⊓ m • a₂ :=
  (smul_mono_right _).map_inf_le _ _

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