Theorems · Theorem · algebraic topology
isCoveringMap_iff_isCoveringMapOn_univ
∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
IsCoveringMap f ↔ IsCoveringMapOn f Set.univ- Defined in
- Mathlib.Topology.Covering.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Set.Elemproof · cited by 7,166
- Set.preimageproof · cited by 4,946
- Set.univstatement · cited by 3,945
- IsCoveringMapstatement · cited by 68
- IsCoveringMapOnstatement · cited by 34
- IsEvenlyCoveredproof · cited by 22
Cited by11
Results whose statement or proof uses this declaration.
- IsAddQuotientCoveringMap.isCoveringMapproof · cited by 16
- IsQuotientCoveringMap.isCoveringMapproof · cited by 15
- IsCoveringMap.comp_homeomorphproof · cited by 5
- IsCoveringMap.isCoveringMapOnproof · cited by 2
- IsCoveringMapOn.isCoveringMap_restrictPreimageproof · cited by 2
- IsCoveringMap.mkproof · cited by 1
- IsCoveringMap.homeomorph_compproof · cited by 1
- isLocalHomeomorph_iff_isCoveringMapproof · cited by 0
- IsCoveringMap.mk'proof · cited by 0
- IsCoveringMap.of_isEmptyproof · cited by 0
- IsCoveringMap.restrictPreimageproof · cited by 0