comap_iInf — Mathlib

English

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

Русский

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

LaTeX

$$$(H \\cap K)^{\\mathrm{comap}\,f} = H^{\\mathrm{comap}\,f} \\cap K^{\\mathrm{comap}\,f}.$$$

Lean4

@[to_additive]
theorem comap_iInf {ι : Sort*} (f : G →* N) (s : ι → Subgroup N) : (iInf s).comap f = ⨅ i, (s i).comap f :=
  (gc_map_comap f).u_iInf

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