Theorems · Definition · general topology

LocallyConstant.comapAddMonoidHom

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {Z : Type u_6} → [inst_2 : AddZeroClass Z] → C(X, Y) → LocallyConstant Y Z →+ LocallyConstant X Z

LocallyConstant.comap as an AddMonoidHom.

Defined in: Mathlib.Topology.LocallyConstant.Algebra
Cited by: 1 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace AddZeroClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

TopologicalSpacestatement and proof · cited by 24,529
AddMonoidHomstatement · cited by 3,230
ContinuousMapstatement and proof · cited by 2,491
AddZeroClassstatement and proof · cited by 1,237
LocallyConstantstatement · cited by 227
LocallyConstant.comapproof · cited by 32

Cited by3

Results whose statement or proof uses this declaration.

LocallyConstant.congrLeftRingEquivproof · cited by 2
LocallyConstant.comapRingHomproof · cited by 1
LocallyConstant.comapAddMonoidHom_applystatement and proof · cited by 0