Theorems · Definition · general topology
LocallyConstant.toFun
{X : Type u_5} → {Y : Type u_6} → [inst : TopologicalSpace X] → LocallyConstant X Y → X → YThe underlying function.
- Defined in
- Mathlib.Topology.LocallyConstant.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- LocallyConstantstatement and proof · cited by 227
Cited by9
Results whose statement or proof uses this declaration.
- LocallyConstant.isLocallyConstantstatement · cited by 7
- LocallyConstant.toFun_eq_coestatement · cited by 2
- Condensed.locallyConstantIsoFinYonedaproof · cited by 2
- Profinite.NobelingProof.coe_πs'statement and proof · cited by 1
- Profinite.NobelingProof.spanFinBasis.spanproof · cited by 1
- Profinite.NobelingProof.factors_prod_eq_basis_of_eqproof · cited by 1
- LightCondensed.locallyConstantIsoFinYonedaproof · cited by 1
- Profinite.NobelingProof.GoodProducts.smaller_monoproof · cited by 1
- CompHausLike.LocallyConstant.unitIsoproof · cited by 0