Theorems · Definition · general topology
IsLocallyInjective
{X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → (X → Y) → PropA function from a topological space X is locally injective if every point of X
has a neighborhood on which f is injective.
- Defined in
- Mathlib.Topology.SeparatedMap
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- IsOpenproof · cited by 2,400
- Set.InjOnproof · cited by 543
Cited by14
Results whose statement or proof uses this declaration.
- IsLocalHomeomorph.isLocallyInjectivestatement · cited by 6
- IsSeparatedMap.eq_of_comp_eqstatement and proof · cited by 4
- isLocallyInjective_iff_isOpen_diagonalstatement · cited by 3
- IsSeparatedMap.const_of_compstatement and proof · cited by 2
- IsSeparatedMap.eqOn_of_comp_eqOnstatement and proof · cited by 2
- IsLocallyInjective_iff_isOpenEmbeddingstatement · cited by 1
- IsLocallyInjective.isOpen_eqLocusstatement and proof · cited by 1
- isLocallyInjective_iff_nhdsstatement and proof · cited by 1
- IsSeparatedMap.constOn_of_compstatement and proof · cited by 1
- Function.Injective.IsLocallyInjectivestatement · cited by 0
- discreteTopology_iff_locallyInjectivestatement and proof · cited by 0
- IsLocallyInjective.comp_leftstatement and proof · cited by 0