map_le_idealRange

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieHom.map_le_idealRange

English

Variant statement asserting the same carrier inclusion for the ideal range.

Русский

Вариант утверждения о включении носителя для диапазона идеала.

LaTeX

$$$\\text{range}(f) \\subseteq \\text{idealRange}(f)$$$

Lean4

theorem map_le_idealRange : I.map f ≤ f.idealRange :=
  by
  rw [f.idealRange_eq_map]
  exact LieIdeal.map_mono le_top

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

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

Разделы

Аффилиация

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