submoduleOf_sup_of_le — Mathlib

English

If N1 ≤ N and N2 ≤ N, then (N1 ⊔ N2).submoduleOf N equals N1.submoduleOf N ⊔ N2.submoduleOf N.

Русский

Если N1 ≤ N и N2 ≤ N, то (N1 ⊔ N2).submoduleOf N = N1.submoduleOf N ⊔ N2.submoduleOf N.

LaTeX

$$$$ N_1 \le N \quad\&\quad N_2 \le N \; \implies\; (N_1 \sqcup N_2).\mathrm{submoduleOf} N = N_1.\mathrm{submoduleOf} N \sqcup N_2.\mathrm{submoduleOf} N $$$$

Lean4

theorem submoduleOf_sup_of_le {N₁ N₂ N : Submodule R M} (h₁ : N₁ ≤ N) (h₂ : N₂ ≤ N) :
    (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N :=
  by
  apply Submodule.map_injective_of_injective N.subtype_injective
  simp only [submoduleOf, map_comap_eq]
  simp_all

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