map_lt_map_iff_of_injective — Mathlib

English

If ker f ≤ H and ker f ≤ K and map f H = map f K, then H = K.

Русский

Если ker f ⊆ H и ker f ⊆ K и map f H = map f K, то H = K.

LaTeX

$$If $\\ker f \\le H$, $\\ker f \\le K$ and $\\operatorname{map} f H = \\operatorname{map} f K$, then $H=K$.$$

Lean4

@[to_additive]
theorem map_lt_map_iff_of_injective {f : G →* N} (hf : Function.Injective f) {H K : Subgroup G} :
    H.map f < K.map f ↔ H < K :=
  lt_iff_lt_of_le_iff_le' (map_le_map_iff_of_injective hf) (map_le_map_iff_of_injective hf)

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