comap_incl_eq_top — Mathlib

English

For LieIdeal I and I₂ with IsIdealMorphism property, comap I.incl I₂ equals the sum I ⊔ I₂.

Русский

Для идеалов I и I₂ с свойством IsIdealMorphism, comap I.incl I₂ равно сумме I ⊔ I₂.

LaTeX

$$$I.incl.IsIdealMorphism \Rightarrow comap I.incl I_2 = I ⊔ I_2$$$

Lean4

@[simp]
theorem comap_incl_eq_top : I₂.comap I.incl = ⊤ ↔ I ≤ I₂ :=
  by
  rw [← LieSubmodule.toSubmodule_inj, LieIdeal.comap_toSubmodule, LieSubmodule.top_toSubmodule, incl_coe]
  simp_rw [toLieSubalgebra_toSubmodule]
  rw [Submodule.comap_subtype_eq_top, LieSubmodule.toSubmodule_le_toSubmodule]

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