map₂_mk_top_top_eq_top — Mathlib

English

Applying the bilinear construction mk to top on both sides yields the top submodule after mapping two factors.

Русский

Применение mk к верхним границам обоих факторов даёт верхнюю подмодуль после отображения двух факторов.

LaTeX

$$$\\mathrm{Submodule.map}_2 (\\mathrm{TensorProduct.mk}\\ R\\ M\\ N) \\top \\top = \\top.$$$

Lean4

@[simp]
theorem map₂_mk_top_top_eq_top : Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤ :=
  by
  rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]
  exact Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, trivial, n, trivial, h⟩

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