Lifting

📁 Source: Mathlib/Topology/Homotopy/Lifting.lean

Statistics

Metric	Count
Definitions Lifting, liftHomotopy, liftHomotopyRel, liftPath, monodromy, monodromyFunctor	6
Theorems eq_liftHomotopy_iff, eq_liftHomotopy_iff', eq_liftPath_iff, eq_liftPath_iff', existsUnique_continuousMap_lifts, existsUnique_continuousMap_lifts_of_range_le, exists_path_lifts, homotopicRel_iff_comp, injective_path_homotopic_map, injective_path_homotopic_mapFn, liftHomotopy_apply, liftHomotopy_lifts, liftHomotopy_zero, liftPath_apply_one_eq_of_homotopicRel, liftPath_const, liftPath_lifts, liftPath_trans, liftPath_zero, monodromyFunctor_map, monodromyFunctor_obj, monodromy_bijective, monodromy_map, monodromy_refl, monodromy_trans_apply, existsUnique_continuousMap_lifts, continuous_lift, existsUnique_continuousMap_lifts, exists_lift_nhds, monodromy_theorem	29
Total	35

CategoryTheory.Localization

Definitions

Name	Category	Theorems
Lifting 📖	CompData	—

IsCoveringMap

Definitions

Name	Category	Theorems
liftHomotopy 📖	CompOp	5 math math: eq_liftHomotopy_iff', liftHomotopy_zero, liftHomotopy_apply, eq_liftHomotopy_iff, liftHomotopy_lifts
liftHomotopyRel 📖	CompOp	—
liftPath 📖	CompOp	8 math math: liftPath_apply_one_eq_of_homotopicRel, liftPath_zero, liftPath_const, eq_liftPath_iff', liftHomotopy_apply, liftPath_lifts, eq_liftPath_iff, liftPath_trans
monodromy 📖	CompOp	5 math math: monodromy_map, monodromy_refl, monodromy_bijective, monodromy_trans_apply, monodromyFunctor_map
monodromyFunctor 📖	CompOp	2 math math: monodromyFunctor_obj, monodromyFunctor_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_liftHomotopy_iff 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftHomotopy Continuous Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing ContinuousMap.continuous_toFun liftHomotopy_lifts liftHomotopy_zero eq_liftPath_iff
eq_liftHomotopy_iff' 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	liftHomotopy Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing Continuous.comp ContinuousMap.continuous_toFun Continuous.prodMk_left
eq_liftPath_iff 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftPath Continuous Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing liftPath_lifts liftPath_zero ContinuousMap.continuous_toFun eq_of_comp_eq ConnectedSpace.toPreconnectedSpace unitInterval.instConnectedSpaceElemReal ContinuousMap.continuous
eq_liftPath_iff' 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	liftPath Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing ContinuousMap.continuous
existsUnique_continuousMap_lifts 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap ContinuousMap.instFunLike	ExistsUnique ContinuousMap DFunLike.coe ContinuousMap.instFunLike	—	IsLocalHomeomorph.existsUnique_continuousMap_lifts isLocalHomeomorph SimplyConnectedSpace.instPathConnectedSpace Real.instIsOrderedRing exists_path_lifts Path.source eq_liftPath_iff' liftPath_apply_one_eq_of_homotopicRel ContinuousMap.HomotopicRel.comp_continuousMap SimplyConnectedSpace.paths_homotopic
existsUnique_continuousMap_lifts_of_range_le 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap ContinuousMap.instFunLike Subgroup FundamentalGroup instGroupFundamentalGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder MonoidHom.range FundamentalGroup.map FundamentalGroup.mapOfEq continuous	ExistsUnique ContinuousMap DFunLike.coe ContinuousMap.instFunLike	—	continuous IsLocalHomeomorph.existsUnique_continuousMap_lifts isLocalHomeomorph Real.instIsOrderedRing exists_path_lifts eq_liftPath_iff' ContinuousMap.continuous monodromy_bijective Path.Homotopic.Quotient.eq Path.Homotopic.Quotient.mk_refl monodromy_refl Path.map_symm Path.map_trans Path.Homotopic.Quotient.mk_surjective monodromy_map Path.Homotopic.Quotient.mk_map FundamentalGroup.map_apply FundamentalGroup.mapOfEq_apply
exists_path_lifts 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing exists_monotone_Icc_subset_open_cover_unitInterval IsOpen.preimage ContinuousMap.continuous Set.mem_iUnion Continuous.continuousOn continuous_const Set.mem_singleton_iff Set.Icc_self le_rfl Set.mem_preimage ContinuousOn.if frontier_Iic_subset Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Bundle.Trivialization.symm_apply_mk_proj Bundle.Trivialization.mem_source ContinuousOn.mono closure_le_eq continuous_id' ContinuousOn.comp OpenPartialHomeomorph.continuousOn_invFun Continuous.comp Continuous.prodMk_left ContinuousMap.continuous_toFun Bundle.Trivialization.target_eq closure_lt_subset_le continuous_subtype_val Bundle.Trivialization.proj_symm_apply' le_of_not_ge continuousOn_univ Set.eq_univ_iff_forall bot_le ZeroLEOneClass.factZeroLeOne Real.instZeroLEOneClass le_top
homotopicRel_iff_comp 📖	mathematical	IsCoveringMap Set Set.instMembership DFunLike.coe ContinuousMap ContinuousMap.instFunLike	ContinuousMap.HomotopicRel ContinuousMap.comp continuous	—	continuous
injective_path_homotopic_map 📖	mathematical	IsCoveringMap	Path.Homotopic.Quotient DFunLike.coe ContinuousMap ContinuousMap.instFunLike continuous Path.Homotopic.Quotient.map	—	continuous ContinuousMap.continuous Path.Homotopic.Quotient.eq Real.instIsOrderedRing homotopicRel_iff_comp ConnectedSpace.toPreconnectedSpace unitInterval.instConnectedSpaceElemReal Path.source
injective_path_homotopic_mapFn 📖	mathematical	IsCoveringMap	Path.Homotopic.Quotient DFunLike.coe ContinuousMap ContinuousMap.instFunLike continuous Path.Homotopic.Quotient.map	—	injective_path_homotopic_map
liftHomotopy_apply 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftHomotopy liftPath ContinuousMap.comp ContinuousMap.prodMk ContinuousMap.id ContinuousMap.const	—	Real.instIsOrderedRing
liftHomotopy_lifts 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftHomotopy	—	Real.instIsOrderedRing liftPath_lifts
liftHomotopy_zero 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftHomotopy Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing liftPath_zero
liftPath_apply_one_eq_of_homotopicRel 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftPath Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing ConnectedSpace.toPreconnectedSpace unitInterval.instConnectedSpaceElemReal liftPath_zero liftPath_lifts ContinuousMap.HomotopyRel.eq_fst ContinuousMap.HomotopyRel.eq_snd
liftPath_const 📖	mathematical	IsCoveringMap	liftPath ContinuousMap.const Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instIsOrderedRing eq_liftPath_iff'
liftPath_lifts 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftPath	—	Real.instIsOrderedRing exists_path_lifts
liftPath_trans 📖	mathematical	IsCoveringMap	liftPath toContinuousMap Path Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.instFunLike Path.continuousMapClass Path.trans ContinuousMap.toFun DFunLike.coe ContinuousMap ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Path.source Set.Icc.instOne liftPath_zero	—	Path.continuousMapClass Real.instIsOrderedRing Path.source liftPath_zero eq_liftPath_iff' Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le Path.trans_apply liftPath_lifts Path.target
liftPath_zero 📖	mathematical	IsCoveringMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike liftPath Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing exists_path_lifts
monodromyFunctor_map 📖	mathematical	IsCoveringMap	CategoryTheory.Functor.map FundamentalGroupoid CategoryTheory.Groupoid.toCategory FundamentalGroupoid.instGroupoid CategoryTheory.types monodromyFunctor monodromy FundamentalGroupoid.as	—	—
monodromyFunctor_obj 📖	mathematical	IsCoveringMap	CategoryTheory.Functor.obj FundamentalGroupoid CategoryTheory.Groupoid.toCategory FundamentalGroupoid.instGroupoid CategoryTheory.types monodromyFunctor Set.Elem Set.preimage Set Set.instSingletonSet FundamentalGroupoid.as	—	—
monodromy_bijective 📖	mathematical	IsCoveringMap	Function.Bijective Set.Elem Set.preimage Set Set.instSingletonSet monodromy	—	CategoryTheory.isIso_iff_bijective CategoryTheory.Functor.map_isIso CategoryTheory.IsGroupoid.all_isIso CategoryTheory.instIsGroupoid
monodromy_map 📖	mathematical	IsCoveringMap	monodromy DFunLike.coe ContinuousMap ContinuousMap.instFunLike continuous Path.Homotopic.Quotient.map Set Set.instMembership Set.preimage Set.instSingletonSet	—	continuous Path.continuousMapClass ContinuousMap.continuous Real.instIsOrderedRing DFunLike.congr_fun eq_liftPath_iff' Path.source Path.target
monodromy_refl 📖	mathematical	IsCoveringMap	monodromy Path.Homotopic.Quotient.refl Set.Elem Set.preimage Set Set.instSingletonSet	—	DFunLike.congr_fun liftPath_const Real.instIsOrderedRing
monodromy_trans_apply 📖	mathematical	IsCoveringMap	monodromy Path.Homotopic.Quotient.trans	—	Path.continuousMapClass Real.instIsOrderedRing Path.source liftPath_zero DFunLike.congr_fun liftPath_trans Path.target

IsCoveringMapOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique_continuousMap_lifts 📖	mathematical	IsCoveringMapOn DFunLike.coe ContinuousMap ContinuousMap.instFunLike Set Set.instMembership	ExistsUnique ContinuousMap DFunLike.coe ContinuousMap.instFunLike	—	continuous_subtype_val ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass CanLift.prf Subtype.canLift Set.mem_preimage IsCoveringMap.existsUnique_continuousMap_lifts isCoveringMap_restrictPreimage ContinuousMap.ext

IsLocalHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_lift 📖	mathematical	IsLocalHomeomorph IsSeparatedMap Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Continuous Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Real.instIsOrderedRing continuous_iff_continuousAt exists_lift_nhds ContinuousOn.continuousAt ContinuousOn.congr IsSeparatedMap.eq_of_comp_eq isLocallyInjective ConnectedSpace.toPreconnectedSpace unitInterval.instConnectedSpaceElemReal ContinuousOn.comp_continuous Continuous.prodMk_left prod_mem_nhds Filter.univ_mem
existsUnique_continuousMap_lifts 📖	mathematical	IsLocalHomeomorph DFunLike.coe ContinuousMap ContinuousMap.instFunLike Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap.comp Set.Icc.instOne	ExistsUnique ContinuousMap DFunLike.coe ContinuousMap.instFunLike	—	Real.instIsOrderedRing Path.source Path.target continuous_iff_continuousAt OpenPartialHomeomorph.map_source ContinuousAt.congr ContinuousAt.comp ContinuousOn.continuousAt OpenPartialHomeomorph.continuousOn_symm IsOpen.mem_nhds OpenPartialHomeomorph.open_target Continuous.continuousAt ContinuousMap.continuous_toFun Filter.HasBasis.mem_iff LocPathConnectedSpace.path_connected_basis IsOpen.preimage ContinuousMap.continuous Filter.mem_of_superset IsPathConnected.joinedIn mem_of_mem_nhds OpenPartialHomeomorph.left_inv Path.continuousMapClass ContinuousOn.comp Continuous.continuousOn Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le Path.trans_apply OpenPartialHomeomorph.right_inv ContinuousMap.comp_const Nontrivial.to_nonempty unitInterval.instNontrivialElemReal DFunLike.ext
exists_lift_nhds 📖	mathematical	IsLocalHomeomorph Set.Elem Real unitInterval DFunLike.coe ContinuousMap instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Continuous Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	Set Filter Filter.instMembership nhds ContinuousOn Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SProd.sprod Set.instSProd Set.univ DFunLike.coe ContinuousMap ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing exists_monotone_Icc_subset_open_cover_unitInterval IsOpen.preimage OpenPartialHomeomorph.open_source Set.mem_iUnion Set.mem_univ isOpen_univ ContinuousOn.congr Continuous.continuousOn Continuous.comp continuous_snd Set.mem_singleton_iff Set.Icc_self OpenPartialHomeomorph.map_source generalized_tube_lemma IsClosed.isCompact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal isClosed_Icc Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology isCompact_singleton ContinuousMap.continuous OpenPartialHomeomorph.open_target Set.singleton_subset_iff le_rfl IsOpen.inter ContinuousOn.isOpen_inter_preimage ContinuousOn.comp Continuous.prodMk_right ContinuousOn.if Set.mem_setOf frontier_le_subset_eq continuous_fst continuous_const OpenPartialHomeomorph.injOn OpenPartialHomeomorph.map_target OpenPartialHomeomorph.right_inv ContinuousOn.mono closure_le_eq OpenPartialHomeomorph.continuousOn_invFun ContinuousMap.continuous_toFun Set.inter_subset_inter_right closure_lt_subset_le ZeroLEOneClass.factZeroLeOne Real.instZeroLEOneClass bot_le le_of_not_ge IsOpen.mem_nhds Set.eq_univ_iff_forall le_top
monodromy_theorem 📖	mathematical	IsLocalHomeomorph IsSeparatedMap DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike ContinuousMap.HomotopyRel Set.instInsert Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.instSingletonSet Set.Icc.instOne ContinuousMap.HomotopyWith.instFunLike	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instZero	—	Real.instIsOrderedRing continuous_lift ContinuousMap.HomotopyLike.toContinuousMapClass ContinuousMap.HomotopyWith.instHomotopyLike continuous_const ContinuousMap.continuous_toFun IsSeparatedMap.const_of_comp isLocallyInjective ConnectedSpace.toPreconnectedSpace unitInterval.instConnectedSpaceElemReal Continuous.comp Continuous.prodMk_right ContinuousMap.HomotopyRel.eq_fst

---

← Back to Index