map_comap_eq

Mathlib.Algebra.Lie.IdealOperations

URI: https://scilib.ai/kg/mathlib#LieSubmodule.map_comap_eq

English

For LieSubmodule N₂, if N₂ ≤ f.range then map f (comap f N₂) = N₂.

Русский

Для подмодуля N₂, если N₂ ⊆ f.range, то map f (comap f N₂) = N₂.

LaTeX

$$$N_2 \le f.\mathrm{range} \Rightarrow \operatorname{map} f (\operatorname{comap} f N_2) = N_2$$$

Lean4

theorem map_comap_eq (hf : N₂ ≤ f.range) : map f (comap f N₂) = N₂ :=
  by
  rw [SetLike.ext'_iff]
  exact Set.image_preimage_eq_of_subset hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru