set_smul_le_iff — Mathlib

English

A leq relation on submodules is preserved by smul with a set S: if p ≤ q then s · p ≤ s · q.

Русский

Отношение ≤ между подмодулями сохраняется при смуле по множеству S: если p ≤ q, то s · p ≤ s · q.

LaTeX

$$$p \\le q \\Rightarrow s \\cdot p \\le s \\cdot q$$$

Lean4

theorem set_smul_le_iff (p : Submodule R M) : s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p :=
  by
  fconstructor
  · intro h r n hr hn
    exact h <| mem_set_smul_of_mem_mem hr hn
  · apply set_smul_le

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