Theorems · Theorem · category theory

GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset

∀ {A B : GrpCat} (f : A ⟶ B) (x : ↑B) (y : ↑(Set.range fun x => x • ↑(GrpCat.Hom.hom f).range)),
  ((GrpCat.SurjectiveOfEpiAuxs.g f) x) (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset y) =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨x • ↑y, ⋯⟩

Defined in: Mathlib.Algebra.Category.Grp.EpiMono
Cited by: 2 results in Mathlib
Foundations: Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Quiver.Homstatement and proof · cited by 32,603
SetLike.coestatement and proof · cited by 8,199
Set.Elemstatement and proof · cited by 7,166
Set.rangestatement and proof · cited by 4,705
MonoidHomstatement · cited by 3,629
Subgroupstatement · cited by 3,593
Equiv.Permstatement · cited by 1,375
Set.smulSetstatement · cited by 608
MonoidHom.rangestatement and proof · cited by 314
GrpCatstatement and proof · cited by 146

Cited by2

Results whose statement or proof uses this declaration.

GrpCat.SurjectiveOfEpiAuxs.agreeproof · cited by 1
GrpCat.SurjectiveOfEpiAuxs.h_apply_infinityproof · cited by 1