comap_incl_eq_top — Mathlib

English

A criterion for inclusion of submodules via comap with inclusion: N ≤ N₂ iff the comap along inclusion is top.

Русский

Критерий включения подмодулей через обратное по включению: N ≤ N₂ тогда и только тогда, что comap по включению равен верхнему.

LaTeX

$$$ N_2.comap N.incl = \top \iff N \le N_2 $$$

Lean4

theorem comap_incl_eq_top : N₂.comap N.incl = ⊤ ↔ N ≤ N₂ := by
  rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
    LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]

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