mem_invtSubmodule_reflection_of_mem

English

If h: f x = 2 and p ⊆ M is a submodule with x ∈ p, then p ∈ End.invtSubmodule (reflection h).

Русский

Пусть h: f x = 2 и p ⊆ M — подсистема с x ∈ p; тогда p инвариантно относительно reflection h.

LaTeX

$$$\\text{If }h:\\ f(x)=2\\text{ and }p\\le M\\text{ with }x\\in p,\\ then\\\\ p\\in End.invtSubmodule(\\mathrm{reflection}(h)).$$$

Lean4

theorem _root_.Submodule.mem_invtSubmodule_reflection_of_mem (h : f x = 2) (p : Submodule R M) (hx : x ∈ p) :
    p ∈ End.invtSubmodule (reflection h) :=
  by
  suffices ∀ y ∈ p, reflection h y ∈ p from (End.mem_invtSubmodule _).mpr fun y hy ↦ by simpa using this y hy
  intro y hy
  simpa only [reflection_apply, p.sub_mem_iff_right hy] using p.smul_mem (f y) hx

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