map_le_range

Mathlib.Algebra.Group.Subgroup.Ker

URI: https://scilib.ai/kg/mathlib#Subgroup.map_le_range

English

Same as the previous statement, in a simplified form.

Русский

То же самое, в упрощенной форме.

LaTeX

$$$\text{Injective}(f) \Rightarrow (\forall H, H.\operatorname{map} f = \bot \iff H = \bot)$$$

Lean4

@[to_additive]
theorem map_le_range (H : Subgroup G) : map f H ≤ f.range :=
  (range_eq_map f).symm ▸ map_mono le_top

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

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

Разделы

Аффилиация

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