localized₀_le_localized₀_of_smul_le

English

If x ∈ p and x•P ≤ Q for submodules P ⊆ M and Q ⊆ M, then their localized₀ images satisfy P.localized₀ p f ≤ Q.localized₀ p f.

Русский

Если x ∈ p и x•P ⊆ Q для подмодулей P ⊆ M и Q ⊆ M, тогда их образи в локализации P.localized₀ p f и Q.localized₀ p f удовлетворяют P.localized₀ p f ⊆ Q.localized₀ p f.

LaTeX

$$$x\in p \implies x\cdot P \subseteq Q \Rightarrow P_{p,f}\subseteq Q_{p,f}$$$

Lean4

theorem localized₀_le_localized₀_of_smul_le {P Q : Submodule R M} (x : p) (h : x • P ≤ Q) :
    P.localized₀ p f ≤ Q.localized₀ p f := by
  rintro - ⟨a, ha, r, rfl⟩
  refine ⟨x • a, h ⟨a, ha, rfl⟩, x * r, ?_⟩
  simp

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