coe_set_smul — Mathlib

English

The HSMul action is covariant with respect to the lattice order, i.e., if I ≤ J then I • N ≤ J • N.

Русский

Действие HSMul корректно относительно порядка: If I ≤ J then I • N ≤ J • N.

LaTeX

$$$I \\le J \\rightarrow N \\le P \\rightarrow I \\!\\cdot\\! N \\le J \\!\\cdot\\! P$$$

Lean4

@[simp, norm_cast]
theorem coe_set_smul : (I : Set A) • N = I • N :=
  set_smul_eq_of_le _ _ _ (fun _ _ hr hx ↦ smul_mem_smul hr hx)
    (smul_le.mpr fun _ hr _ hx ↦ mem_set_smul_of_mem_mem hr hx)

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