map_le_map_iff' — Mathlib

English

For subgroups H,K of G, H.map f = K.map f if and only if H ⊔ ker f = K ⊔ ker f.

Русский

Для подгрупп H,K ⊆ G: H.map f = K.map f эквивалентно H ⊔ ker f = K ⊔ ker f.

LaTeX

$$$H.map f = K.map f \\iff H \\sqcup \\ker f = K \\sqcup \\ker f$$$

Lean4

@[to_additive]
theorem map_le_map_iff' {f : G →* N} {H K : Subgroup G} : H.map f ≤ K.map f ↔ H ⊔ f.ker ≤ K ⊔ f.ker := by
  simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]

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