comap_map_le

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieIdeal.comap_map_le

English

For LieIdeal I, we have comap f (map f I) ≥ I.

Русский

Для идеала I верно, что comap f (map f I) своей величиной не меньше I.

LaTeX

$$$I \\le \\mathrm{comap}(f,\\mathrm{map}(f,I))$$$

Lean4

/-- See also `LieIdeal.map_comap_eq`. -/
theorem comap_map_le : I ≤ comap f (map f I) := by rw [← map_le_iff_le_comap]

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

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

Разделы

Аффилиация

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