Theorems · Theorem · group theory

Subgroup.map_iInf

∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {ι : Sort u_7} [Nonempty ι] (f : G →* N),
  Function.Injective ⇑f → ∀ (s : ι → Subgroup G), Subgroup.map f (iInf s) = ⨅ i, Subgroup.map f (s i)

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroupNonempty