map_inf_le — Mathlib

English

For subgroups H, K of G and f: G →* N, map f (H ⊓ K) ≤ map f H ⊓ map f K.

Русский

Для подгрупп H, K ⊆ G и f: G →* N выполняется map f (H ∩ K) ≤ map f H ∩ map f K.

LaTeX

$$$\\mathrm{map}_f(H \\cap K) \\le \\mathrm{map}_f(H) \\cap \\mathrm{map}_f(K).$$$

Lean4

@[to_additive]
theorem map_inf_le (H K : Subgroup G) (f : G →* N) : map f (H ⊓ K) ≤ map f H ⊓ map f K :=
  le_inf (map_mono inf_le_left) (map_mono inf_le_right)

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