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`	`liftHomotopy` `Continuous`	—	`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`	—	`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`	`liftPath` `Continuous`	—	`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`	—	`Real.instIsOrderedRing` `ContinuousMap.continuous`
`existsUnique_continuousMap_lifts` 📖	mathematical	`IsCoveringMap` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`ExistsUnique`	—	`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`	—	`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` 📖	—	`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`	—	—	`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` `Trivialization.symm_apply_mk_proj` `Trivialization.mem_source` `ContinuousOn.mono` `closure_le_eq` `continuous_id'` `ContinuousOn.comp` `OpenPartialHomeomorph.continuousOn_invFun` `Continuous.comp` `Continuous.prodMk_left` `ContinuousMap.continuous_toFun` `Trivialization.target_eq` `closure_lt_subset_le` `continuous_subtype_val` `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`	`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`	`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`	`liftHomotopy`	—	`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`	`liftPath` `Set.Icc.instOne`	—	`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`	`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`	`liftPath`	—	`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`	—	`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` 📖	—	`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`	—	—	`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`	—	`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`	`Filter` `Filter.instMembership` `nhds` `ContinuousOn` `SProd.sprod` `Set.instSProd` `Set.univ`	—	`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` 📖	—	`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`	—	—	`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