map_inf — Mathlib

English

If H, K are subgroups of G and f is injective, then (H ⊓ K).map f = H.map f ⊓ K.map f.

Русский

Если H, K — подгруппы G, и f инъективен, то (H ⊓ K).map f = H.map f ⊓ K.map f.

LaTeX

$$$(H \\cap K).\\mathrm{map}(f) = H.map(f) \\cap K.map(f)$, assuming injective f.$$

Lean4

@[to_additive]
theorem map_inf (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) : (H ⊓ K).map f = H.map f ⊓ K.map f :=
  SetLike.coe_injective (Set.image_inter hf)

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