mem_support_mono — Mathlib

English

If p ≤ q and p lies in the support of M, then q also lies in the support of M.

Русский

Если p ⊆ q и p принадлежит опоре M, то и q принадлежит опоре M.

LaTeX

$$$p \le q \implies p \in \mathrm{Supp}_R(M) \Rightarrow q \in \mathrm{Supp}_R(M)$$$

Lean4

theorem mem_support_mono {p q : PrimeSpectrum R} (H : p ≤ q) (hp : p ∈ Module.support R M) : q ∈ Module.support R M :=
  by
  rw [Module.mem_support_iff_exists_annihilator] at hp ⊢
  exact ⟨_, hp.choose_spec.trans H⟩

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