localized'_le_localized'_of_smul_le

English

A variant of monotonicity: if x ∈ p and x•P ≤ Q then P.localized′ S p f ≤ Q.localized′ S p f.

Русский

Вариант монотонности: если x ∈ p и x•P ≤ Q, то P.localized′ S p f ≤ Q.localized′ S p f.

LaTeX

$$$x\in p \land x\cdot P \le Q \Rightarrow P_{S,p,f} \le Q_{S,p,f}$$$

Lean4

theorem localized'_le_localized'_of_smul_le {P Q : Submodule R M} (x : p) (h : x • P ≤ Q) :
    P.localized' S p f ≤ Q.localized' S p f :=
  localized₀_le_localized₀_of_smul_le p f x h

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