Basic

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

Statistics

Metric	Count
Definitions Homotopic, HomotopicRel, HomotopicWith, apply, cast, comp, compContinuousMap, curry, extend, instFunLike, instInhabitedId, pi, piMap, prodMap, prodMk, refl, toContinuousMap, trans, HomotopyLike, HomotopyRel, cast, compContinuousMap, refl, trans, HomotopyWith, apply, cast, instFunLike, instInhabitedIdTrue, refl, toHomotopy, trans	32
Theorems comp, equivalence, pi, piMap, prodMap, prodMk, refl, trans, comp_continuousMap, equivalence, homotopic, refl, trans, refl, trans, apply_one, apply_zero, cast_apply, coe_toContinuousMap, compContinuousMap_apply, comp_apply, congr_arg, congr_fun, continuous, curry_apply, curry_one, curry_zero, ext, ext_iff, extend_apply_coe, extend_apply_of_le_zero, extend_apply_of_mem_I, extend_apply_of_one_le, extend_of_mem_I, extend_one, extend_zero, instHomotopyLike, map_one_left, map_zero_left, refl_apply, symm_apply, symm_bijective, symm_symm, symm_trans, trans_apply, map_one_left, map_zero_left, toContinuousMapClass, cast_apply, compContinuousMap_apply, eq_fst, eq_snd, fst_eq_snd, refl_apply, symm_apply, symm_bijective, symm_symm, symm_trans, trans_apply, apply_one, apply_zero, cast_apply, coeFn_injective, coe_toContinuousMap, coe_toHomotopy, continuous, ext, ext_iff, extendProp, instHomotopyLike, prop, prop', refl_apply, symm_apply, symm_bijective, symm_symm, symm_trans, trans_apply, homotopicRel_empty	79
Total	111

ContinuousMap

Definitions

Name	Category	Theorems
Homotopic 📖	MathDef	12 math math: Homotopic.comp, HomotopyEquiv.right_inv, homotopicRel_empty, Homotopic.symm, HomotopyEquiv.left_inv, Homotopic.prodMap, Homotopic.trans, homotopic_const_iff, Homotopic.equivalence, HomotopicRel.homotopic, Homotopic.prodMk, Homotopic.refl
HomotopicRel 📖	MathDef	7 math math: HomotopicRel.comp_continuousMap, HomotopicRel.trans, homotopicRel_empty, HomotopicRel.equivalence, HomotopicRel.refl, IsCoveringMap.homotopicRel_iff_comp, HomotopicRel.symm
HomotopicWith 📖	MathDef	3 math math: HomotopicWith.refl, HomotopicWith.symm, HomotopicWith.trans
HomotopyLike 📖	CompData	2 math math: Homotopy.instHomotopyLike, HomotopyWith.instHomotopyLike
HomotopyRel 📖	CompOp	5 math math: GenLoop.homotopyTo_apply, HomotopyRel.trans_apply, HomotopyRel.symm_bijective, HomotopyRel.eq_fst, HomotopyRel.eq_snd
HomotopyWith 📖	CompData	25 math math: HomotopyRel.prod_apply, HomotopyWith.coe_toContinuousMap, HomotopyWith.symm_bijective, Path.Homotopy.map_apply, HomotopyWith.apply_one, HomotopyRel.refl_apply, Path.Homotopy.symm_apply, HomotopyRel.compContinuousMap_apply, HomotopyWith.coeFn_injective, HomotopyWith.trans_apply, HomotopyRel.symm_apply, Path.Homotopy.cast_apply, HomotopyWith.ext_iff, HomotopyWith.refl_apply, HomotopyWith.symm_apply, HomotopyWith.continuous, HomotopyRel.cast_apply, HomotopyWith.coe_toHomotopy, HomotopyWith.apply_zero, HomotopyWith.cast_apply, Path.Homotopy.symm₂_apply, HomotopyRel.pi_apply, Path.Homotopy.refl_apply, GenLoop.homotopyFrom_apply, HomotopyWith.instHomotopyLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homotopicRel_empty 📖	mathematical	—	HomotopicRel Set Set.instEmptyCollection Homotopic	—	HomotopicRel.homotopic Continuous.comp continuous_toFun

ContinuousMap.Homotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	ContinuousMap.Homotopic ContinuousMap.comp	—	Nonempty.map2
equivalence 📖	mathematical	—	ContinuousMap ContinuousMap.Homotopic	—	refl symm trans
pi 📖	mathematical	ContinuousMap.Homotopic	Pi.topologicalSpace ContinuousMap.pi	—	—
piMap 📖	mathematical	ContinuousMap.Homotopic	Pi.topologicalSpace ContinuousMap.piMap	—	pi comp refl
prodMap 📖	mathematical	—	ContinuousMap.Homotopic instTopologicalSpaceProd ContinuousMap.prodMap	—	—
prodMk 📖	mathematical	—	ContinuousMap.Homotopic instTopologicalSpaceProd ContinuousMap.prodMk	—	—
refl 📖	mathematical	—	ContinuousMap.Homotopic	—	—
trans 📖	mathematical	—	ContinuousMap.Homotopic	—	Nonempty.map2

ContinuousMap.HomotopicRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_continuousMap 📖	mathematical	—	ContinuousMap.HomotopicRel ContinuousMap.comp	—	Nonempty.map
equivalence 📖	mathematical	—	ContinuousMap ContinuousMap.HomotopicRel	—	refl symm trans
homotopic 📖	mathematical	—	ContinuousMap.Homotopic	—	Nonempty.map
refl 📖	mathematical	—	ContinuousMap.HomotopicRel	—	—
trans 📖	mathematical	—	ContinuousMap.HomotopicRel	—	Nonempty.map2

ContinuousMap.HomotopicWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	ContinuousMap.HomotopicWith	—	—
trans 📖	mathematical	—	ContinuousMap.HomotopicWith	—	—

ContinuousMap.Homotopy

Definitions

Name	Category	Theorems
cast 📖	CompOp	1 math math: cast_apply
comp 📖	CompOp	1 math math: comp_apply
compContinuousMap 📖	CompOp	1 math math: compContinuousMap_apply
curry 📖	CompOp	6 math math: Path.Homotopy.eval_apply, curry_apply, extend_of_mem_I, ContinuousMap.HomotopyWith.prop, curry_one, curry_zero
extend 📖	CompOp	9 math math: extend_apply_of_one_le, pathExtend_evalAt, extend_apply_coe, ContinuousMap.HomotopyWith.extendProp, extend_apply_of_mem_I, extend_of_mem_I, extend_zero, extend_one, extend_apply_of_le_zero
instFunLike 📖	CompOp	26 math math: apply_zero_path, evalAt_eq, ulift_apply, cast_apply, Path.toHomotopyConst_apply, compContinuousMap_apply, comp_apply, apply_one_path, instHomotopyLike, extend_apply_coe, evalAt_apply, symm_apply, trans_apply, curry_apply, extend_apply_of_mem_I, continuous, affine_apply, coe_toContinuousMap, apply_zero, prod_apply, apply_one, congr_fun, ext_iff, ContinuousMap.HomotopyWith.coe_toHomotopy, refl_apply, congr_arg
instInhabitedId 📖	CompOp	—
pi 📖	CompOp	—
piMap 📖	CompOp	—
prodMap 📖	CompOp	—
prodMk 📖	CompOp	—
refl 📖	CompOp	1 math math: refl_apply
toContinuousMap 📖	CompOp	5 math math: ContinuousMap.HomotopyWith.coe_toContinuousMap, ContinuousMap.HomotopyWith.prop', coe_toContinuousMap, map_one_left, map_zero_left
trans 📖	CompOp	2 math math: symm_trans, trans_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_one 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	map_one_left
apply_zero 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	map_zero_left
cast_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike cast	—	—
coe_toContinuousMap 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike toContinuousMap ContinuousMap.Homotopy instFunLike	—	—
compContinuousMap_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy ContinuousMap.comp Set.Elem Real unitInterval instFunLike compContinuousMap ContinuousMap ContinuousMap.instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy ContinuousMap.comp Set.Elem Real unitInterval instFunLike comp	—	—
congr_arg 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike	—	ContinuousMap.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike	—	ContinuousMap.congr_fun
continuous 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap.Homotopy instFunLike	—	ContinuousMap.continuous_toFun
curry_apply 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen curry ContinuousMap.Homotopy instFunLike	—	—
curry_one 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike curry Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	ContinuousMap.ext Real.instIsOrderedRing apply_one
curry_zero 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike curry Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	ContinuousMap.ext Real.instIsOrderedRing apply_zero
ext 📖	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike	—	ext
extend_apply_coe 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen extend Set Set.instMembership unitInterval ContinuousMap.Homotopy Set.Elem instFunLike	—	ContinuousMap.congr_fun zero_le_one' Real.instZeroLEOneClass Set.IccExtend_val
extend_apply_of_le_zero 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe ContinuousMap ContinuousMap.instFunLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen extend	—	Real.instIsOrderedRing apply_zero ContinuousMap.congr_fun zero_le_one' Real.instZeroLEOneClass Set.left_mem_Icc Set.IccExtend_of_le_left
extend_apply_of_mem_I 📖	mathematical	Real Set Set.instMembership unitInterval	DFunLike.coe ContinuousMap ContinuousMap.instFunLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen extend ContinuousMap.Homotopy Set.Elem instFunLike	—	extend_of_mem_I
extend_apply_of_one_le 📖	mathematical	Real Real.instLE Real.instOne	DFunLike.coe ContinuousMap ContinuousMap.instFunLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen extend	—	Real.instIsOrderedRing apply_one ContinuousMap.congr_fun zero_le_one' Real.instZeroLEOneClass Set.right_mem_Icc Set.IccExtend_of_right_le
extend_of_mem_I 📖	mathematical	Real Set Set.instMembership unitInterval	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike extend Set.Elem instTopologicalSpaceSubtype curry	—	Set.IccExtend_of_mem zero_le_one' Real.instZeroLEOneClass
extend_one 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike extend Real.instOne	—	Real.instZeroLEOneClass extend_of_mem_I curry_one
extend_zero 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike extend Real.instZero	—	Real.instZeroLEOneClass extend_of_mem_I curry_zero
instHomotopyLike 📖	mathematical	—	ContinuousMap.HomotopyLike ContinuousMap.Homotopy instFunLike	—	ContinuousMap.continuous_toFun map_zero_left map_one_left
map_one_left 📖	mathematical	—	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toContinuousMap Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	—
map_zero_left 📖	mathematical	—	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toContinuousMap Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	—
refl_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike refl ContinuousMap ContinuousMap.instFunLike	—	—
symm_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike symm unitInterval.symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective ContinuousMap.Homotopy symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	ext unitInterval.symm_symm
symm_trans 📖	mathematical	—	symm trans	—	ext 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 trans_apply symm_apply Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_eq apply_one unitInterval.symm_one apply_zero Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Linarith.add_neg lt_of_not_ge
trans_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval instFunLike trans Real.instLE Set Set.instMembership DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Real.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Set.Icc Real.instPreorder Real.instZero unitInterval.mul_pos_mem_iff zero_lt_two Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Ring.toSemiring Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instIsOrderedAddMonoid Preorder.toLE Real.instSub unitInterval.two_mul_sub_one_mem_iff LT.lt.le PartialOrder.toPreorder LinearOrder.toPartialOrder Real.linearOrder Preorder.toLT not_le	—	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 instOrderTopologyReal extend.eq_1 ContinuousMap.coe_IccExtend Set.IccExtend_of_mem

ContinuousMap.Homotopy.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

ContinuousMap.HomotopyLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_one_left 📖	mathematical	—	DFunLike.coe Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	—
map_zero_left 📖	mathematical	—	DFunLike.coe Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	—
toContinuousMapClass 📖	mathematical	—	ContinuousMapClass Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—

ContinuousMap.HomotopyRel

Definitions

Name	Category	Theorems
cast 📖	CompOp	1 math math: cast_apply
compContinuousMap 📖	CompOp	1 math math: compContinuousMap_apply
refl 📖	CompOp	1 math math: refl_apply
trans 📖	CompOp	2 math math: trans_apply, symm_trans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike cast	—	—
compContinuousMap_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith ContinuousMap.comp Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike compContinuousMap ContinuousMap ContinuousMap.instFunLike	—	—
eq_fst 📖	mathematical	Set Set.instMembership	DFunLike.coe ContinuousMap.HomotopyRel Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike ContinuousMap ContinuousMap.instFunLike	—	ContinuousMap.HomotopyWith.prop
eq_snd 📖	mathematical	Set Set.instMembership	DFunLike.coe ContinuousMap.HomotopyRel Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike ContinuousMap ContinuousMap.instFunLike	—	eq_fst Real.instIsOrderedRing ContinuousMap.HomotopyWith.apply_one
fst_eq_snd 📖	mathematical	Set Set.instMembership	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	—	Real.instIsOrderedRing eq_snd eq_fst
refl_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike refl ContinuousMap ContinuousMap.instFunLike	—	—
symm_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike symm unitInterval.symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective ContinuousMap.HomotopyRel symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	ContinuousMap.HomotopyWith.symm_symm
symm_trans 📖	mathematical	—	symm trans	—	ContinuousMap.HomotopyWith.ext ContinuousMap.Homotopy.congr_fun ContinuousMap.Homotopy.symm_trans
trans_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyRel Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike trans Real.instLE Set Set.instMembership DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Real.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Set.Icc Real.instPreorder Real.instZero unitInterval.mul_pos_mem_iff zero_lt_two Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Ring.toSemiring Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instIsOrderedAddMonoid Preorder.toLE Real.instSub unitInterval.two_mul_sub_one_mem_iff LT.lt.le PartialOrder.toPreorder LinearOrder.toPartialOrder Real.linearOrder Preorder.toLT not_le	—	ContinuousMap.Homotopy.trans_apply

ContinuousMap.HomotopyWith

Definitions

Name	Category	Theorems
cast 📖	CompOp	1 math math: cast_apply
instFunLike 📖	CompOp	35 math math: ContinuousMap.HomotopyRel.prod_apply, coe_toContinuousMap, Path.Homotopy.map_apply, GenLoop.homotopyTo_apply, Path.Homotopy.target, apply_one, ContinuousMap.HomotopyRel.refl_apply, ContinuousMap.HomotopyRel.trans_apply, Path.Homotopy.hcomp_half, Path.Homotopy.hcomp_apply, Path.Homotopy.symm_apply, ContinuousMap.HomotopyRel.compContinuousMap_apply, coeFn_injective, trans_apply, Path.Homotopy.trans_apply, ContinuousMap.HomotopyRel.symm_apply, Path.Homotopy.cast_apply, Path.Homotopy.coeFn_injective, ext_iff, refl_apply, symm_apply, continuous, ContinuousMap.HomotopyRel.cast_apply, coe_toHomotopy, ContinuousMap.HomotopyRel.eq_fst, Path.Homotopy.source, apply_zero, cast_apply, Path.Homotopy.symm₂_apply, ContinuousMap.HomotopyRel.pi_apply, Path.Homotopy.refl_apply, GenLoop.homotopyFrom_apply, instHomotopyLike, ContinuousMap.HomotopyRel.eq_snd, isSimplyConnected_iff_exists_homotopy_refl_forall_mem
instInhabitedIdTrue 📖	CompOp	—
refl 📖	CompOp	1 math math: refl_apply
toHomotopy 📖	CompOp	6 math math: coe_toContinuousMap, prop', Path.Homotopy.eval_apply, extendProp, prop, coe_toHomotopy
trans 📖	CompOp	2 math math: symm_trans, trans_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_one 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	ContinuousMap.Homotopy.map_one_left
apply_zero 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing ContinuousMap ContinuousMap.instFunLike	—	ContinuousMap.Homotopy.map_zero_left
cast_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike cast	—	—
coeFn_injective 📖	mathematical	—	ContinuousMap.HomotopyWith DFunLike.coe Set.Elem Real unitInterval instFunLike	—	DFunLike.coe_injective'
coe_toContinuousMap 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike ContinuousMap.Homotopy.toContinuousMap toHomotopy ContinuousMap.HomotopyWith instFunLike	—	—
coe_toHomotopy 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy Set.Elem Real unitInterval ContinuousMap.Homotopy.instFunLike toHomotopy ContinuousMap.HomotopyWith instFunLike	—	—
continuous 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap.HomotopyWith instFunLike	—	ContinuousMap.continuous_toFun
ext 📖	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike	—	ext
extendProp 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike ContinuousMap.Homotopy.extend toHomotopy	—	prop
instHomotopyLike 📖	mathematical	—	ContinuousMap.HomotopyLike ContinuousMap.HomotopyWith instFunLike	—	ContinuousMap.continuous_toFun ContinuousMap.Homotopy.map_zero_left ContinuousMap.Homotopy.map_one_left
prop 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instFunLike ContinuousMap.Homotopy.curry toHomotopy	—	prop'
prop' 📖	mathematical	—	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.Homotopy.toContinuousMap toHomotopy Continuous.comp ContinuousMap.continuous_toFun	—	—
refl_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike refl ContinuousMap ContinuousMap.instFunLike	—	—
symm_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike symm unitInterval.symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective ContinuousMap.HomotopyWith symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	ext ContinuousMap.Homotopy.congr_fun ContinuousMap.Homotopy.symm_symm
symm_trans 📖	mathematical	—	symm trans	—	ext ContinuousMap.Homotopy.congr_fun ContinuousMap.Homotopy.symm_trans
trans_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instFunLike trans Real.instLE Set Set.instMembership DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Real.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Set.Icc Real.instPreorder Real.instZero unitInterval.mul_pos_mem_iff zero_lt_two Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Ring.toSemiring Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instIsOrderedAddMonoid Preorder.toLE Real.instSub unitInterval.two_mul_sub_one_mem_iff LT.lt.le PartialOrder.toPreorder LinearOrder.toPartialOrder Real.linearOrder Preorder.toLT not_le	—	ContinuousMap.Homotopy.trans_apply

ContinuousMap.HomotopyWith.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

---

← Back to Index