Theorems · Theorem · group theory

Subgroup.map_inf_le

∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H K : Subgroup G) (f : G →* N),
  Subgroup.map f (H ⊓ K) ≤ Subgroup.map f H ⊓ Subgroup.map f K

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupGroup