strictMono_comap_prod_map — Mathlib

English

The map m ↦ (comap p.subtype m, map p.mkQ m) from submodules of M to a product is strictly monotone.

Русский

Отображение m ↦ (comap p.subtype m, map p.mkQ m) из подмодулов M в произведение является строго монотонным.

LaTeX

$$$$ \\operatorname{StrictMono} \\bigl( m \\mapsto (\\operatorname{comap} p.subtype\, m,\; \\operatorname{map} p.mkQ\, m) \\bigr). $$$$

Lean4

theorem strictMono_comap_prod_map : StrictMono fun m : Submodule R M ↦ (m.comap p.subtype, m.map p.mkQ) := fun m₁ m₂ ↦
  QuotientAddGroup.strictMono_comap_prod_map p.toAddSubgroup (a := m₁.toAddSubgroup) (b := m₂.toAddSubgroup)

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