Path

📁 Source: Mathlib/Topology/Path.lean

Statistics

Metric	Count
Definitions add, cast, extend, id, instFunLike, instHasUncurryPath, instTopologicalSpace, inv, map, map', mul, neg, ofLine, pi, prod, refl, reparam, apply, toContinuousMap, trans, truncate, truncateOfLE	22
Theorems pathExtend, path_trans, pathExtend, pathExtend, add_apply, bijective_cast, cast_coe, cast_rfl_rfl, cast_symm, cast_trans, coe_mk', coe_mk_mk, coe_reparam, coe_toContinuousMap, continuous, continuousMapClass, continuous_extend, continuous_symm, continuous_trans, continuous_uncurry_extend_of_continuous_family, continuous_uncurry_iff, exists_congr, ext, ext_iff, extend_apply, extend_cast, extend_extends, extend_extends', extend_of_le_zero, extend_of_one_le, extend_one, extend_range, extend_symm, extend_symm_apply, extend_trans_of_half_le, extend_trans_of_le_half, extend_zero, id_apply, image_extend_of_subset, instContinuousEvalElemRealUnitInterval, inv_apply, map_coe, map_id, map_map, map_symm, map_trans, mul_apply, neg_apply, ofLine_extend, ofLine_mem, pi_coe, prod_coe, range_coe, range_reparam, refl_apply, refl_extend, refl_range, refl_reparam, refl_symm, refl_trans_refl, reparam_id, source, source', source_mem_range, symm_apply, symm_bijective, symm_cast, symm_continuous_family, symm_range, symm_symm, target, target', target_mem_range, trans_apply, trans_cast, trans_continuous_family, trans_pi_eq_pi_trans, trans_prod_eq_prod_trans, trans_range, trans_symm, truncate_const_continuous_family, truncate_continuous_family, truncate_one_one, truncate_range, truncate_self, truncate_zero_one, truncate_zero_zero	87
Total	109

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathExtend 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry Path.instHasUncurryPath	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Path.extend	—	IccExtend instOrderTopologyReal
path_trans 📖	mathematical	Continuous Path Path.instTopologicalSpace	Path.trans	—	Path.continuous_uncurry_iff Path.trans_continuous_family

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathExtend 📖	mathematical	ContinuousAt Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry Path.instHasUncurryPath Set.projIcc Real.linearOrder Real.instZero Real.instOne zero_le_one Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.instZeroLEOneClass	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Path.extend	—	zero_le_one Real.instZeroLEOneClass IccExtend instOrderTopologyReal

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathExtend 📖	mathematical	Filter.Tendsto Set.Elem Real unitInterval Function.HasUncurry.uncurry Path.instHasUncurryPath SProd.sprod Filter Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Real.linearOrder Real.instZero Real.instOne Filter.instSProd nhds Filter.map Set.projIcc zero_le_one Preorder.toLE Real.instZeroLEOneClass	Function.hasUncurryInduction Function.hasUncurryBase DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Path.extend	—	zero_le_one Real.instZeroLEOneClass IccExtend

Path

Definitions

Name	Category	Theorems
add 📖	CompOp	2 math math: add_apply, segment_add_segment
cast 📖	CompOp	25 math math: FundamentalGroupoid.eqToHom_eq, bijective_cast, FundamentalGroupoid.conj_eqToHom_assoc, exists_congr, cast_rfl_rfl, Homotopic.pathCast, truncate_self, cast_coe, truncate_zero_zero, curveIntegralFun_cast, cast_trans, FundamentalGroup.mapOfEq_apply, symm_cast, curveIntegrable_cast_iff, truncate_zero_one, FundamentalGroupoid.conj_eqToHom, Homotopic.Quotient.mk_cast, curveIntegral_cast, cast_symm, trans_cast, subpath_zero_one, truncate_one_one, CurveIntegrable.cast, cast_segment, extend_cast
extend 📖	CompOp	35 math math: extend_extends, ofLine_extend, extend_symm_apply, truncate_self, continuous_extend, extend_trans_of_le_half, Continuous.pathExtend, extend_apply, ContinuousMap.Homotopy.pathExtend_evalAt, uniformContinuous_extend_left, truncate_zero_zero, extend_of_one_le, image_extend_of_subset, ContinuousAt.pathExtend, extend_range, curveIntegralFun_def', continuous_uncurry_extend_of_continuous_family, truncate_zero_one, extend_one, curveIntegral_eq_intervalIntegral_deriv, extend_symm, extend_zero, truncate_const_continuous_family, extend_extends', truncate_continuous_family, Filter.Tendsto.pathExtend, extend_of_le_zero, truncate_one_one, uniformContinuous_extend, extend_trans_of_half_le, refl_extend, curveIntegralFun_def, truncate_range, eqOn_extend_segment, extend_cast
id 📖	CompOp	1 math math: id_apply
instFunLike 📖	CompOp	66 math math: subpath_self, IsPathConnected.exists_path_through_family', continuousMapClass, extend_extends, GenLoop.fromLoop_apply, selfAdjoint.expUnitaryPathToOne_apply, range_subpath_of_ge, pi_coe, ext_iff, toHomotopyConst_apply, extend_apply, cast_coe, ofLine_mem, Homotopy.hcomp_apply, instContinuousEvalElemRealUnitInterval, Homotopy.eval_apply, IsPathConnected.exists_path_through_family, mul_apply, ContinuousMap.Homotopy.evalAt_apply, uniformContinuous, image_extend_of_subset, GenLoop.toLoop_apply, extend_range, isUniformEmbedding_coe, range_subpath, symm_apply, inv_apply, refl_apply, range_segment, prod_coe, Manifold.riemannianEDist_def, GenLoop.toLoop_apply_coe, range_reparam, continuous, source_mem_range, neg_apply, target_mem_range, PathConnectedSpace.exists_path_through_family, trans_apply, trans_range, symm_subpath, PathConnectedSpace.exists_path_through_family', coe_mk_mk, range_coe, add_apply, map_coe, subpath_continuous_family, JoinedIn.somePath_mem, refl_range, id_apply, source, coe_toContinuousMap, extend_extends', truncate_continuous_family, target, subpath_zero_one, range_subpath_of_le, segment_apply, coe_reparam, coe_mk', Homotopy.refl_apply, symm_range, Unitary.path_apply, truncate_range, Homotopic.concat_subpath, IsCoveringMap.liftPath_trans
instHasUncurryPath 📖	CompOp	2 math math: continuous_uncurry_iff, truncate_const_continuous_family
instTopologicalSpace 📖	CompOp	10 math math: GenLoop.loopHomeo_apply, continuous_symm, continuous_delayReflRight, continuous_delayReflLeft, instContinuousEvalElemRealUnitInterval, GenLoop.continuous_fromLoop, continuous_uncurry_iff, GenLoop.loopHomeo_symm_apply, continuous_trans, GenLoop.continuous_toLoop
inv 📖	CompOp	1 math math: inv_apply
map 📖	CompOp	11 math math: Homotopic.map_lift, Homotopy.map_apply, Homotopic.map, Homotopic.map_trans_evalAt, Homotopic.Quotient.mk_map, FundamentalGroup.mapOfEq_apply, map_trans, map_id, map_coe, map_symm, map_map
map' 📖	CompOp	—
mul 📖	CompOp	1 math math: mul_apply
neg 📖	CompOp	1 math math: neg_apply
ofLine 📖	CompOp	2 math math: ofLine_extend, ofLine_mem
pi 📖	CompOp	3 math math: pi_coe, trans_pi_eq_pi_trans, Homotopic.pi_lift
prod 📖	CompOp	3 math math: trans_prod_eq_prod_trans, prod_coe, Homotopic.prod_lift
refl 📖	CompOp	28 math math: FundamentalGroupoid.eqToHom_eq, subpath_self, delayReflRight_zero, truncate_self, curveIntegralFun_refl, Homotopic.trans_symm, truncate_zero_zero, Homotopic.refl_trans, concat_zero, delayReflLeft_zero, segment_same, refl_apply, CurveIntegrable.refl, curveIntegral_refl, Homotopic.trans_refl, Homotopic.symm_trans, refl_symm, refl_trans_refl, refl_range, Homotopy.trans_refl_reparam, refl_reparam, FundamentalGroupoid.id_eq_path_refl, concat_refl, truncate_one_one, simply_connected_iff_loops_nullhomotopic, refl_extend, Homotopic.Quotient.mk_refl, isSimplyConnected_iff_exists_homotopy_refl_forall_mem
reparam 📖	CompOp	6 math math: reparam_id, Homotopy.trans_assoc_reparam, range_reparam, Homotopy.trans_refl_reparam, refl_reparam, coe_reparam
toContinuousMap 📖	CompOp	18 math math: Homotopy.map_apply, Homotopy.target, Homotopy.hcomp_half, Homotopy.hcomp_apply, Homotopy.symm_apply, Homotopy.eval_apply, source', Homotopy.trans_apply, Homotopy.cast_apply, Homotopy.coeFn_injective, target', coe_toContinuousMap, Homotopy.source, Homotopy.symm₂_apply, Homotopy.refl_apply, GenLoop.homotopyFrom_apply, GenLoop.fromLoop_coe, isSimplyConnected_iff_exists_homotopy_refl_forall_mem
trans 📖	CompOp	42 math math: Homotopic.trans_assoc, Homotopic.comp_lift, delayReflRight_zero, trans_pi_eq_pi_trans, curveIntegralFun_trans_aeeq_right, extend_trans_of_le_half, Homotopic.trans_symm, Homotopy.hcomp_half, Homotopy.hcomp_apply, Homotopic.map_trans_evalAt, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left, Homotopic.refl_trans, Homotopy.trans_assoc_reparam, cast_trans, curveIntegralFun_trans_of_half_lt, delayReflLeft_zero, concat_succ, trans_prod_eq_prod_trans, uniformContinuous_trans, Continuous.path_trans, curveIntegral_trans, trans_continuous_family, map_trans, Homotopic.trans_refl, Homotopic.symm_trans, trans_symm, trans_apply, trans_range, continuous_trans, refl_trans_refl, Homotopic.Quotient.mk_trans, Homotopic.hcomp, curveIntegralFun_trans_aeeq_left, Homotopy.trans_refl_reparam, trans_cast, CurveIntegrable.trans, curveIntegralFun_trans_of_lt_half, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_right, GenLoop.fromLoop_trans_toLoop, extend_trans_of_half_le, Homotopic.concat_two, IsCoveringMap.liftPath_trans
truncate 📖	CompOp	7 math math: truncate_self, truncate_zero_zero, truncate_zero_one, truncate_const_continuous_family, truncate_continuous_family, truncate_one_one, truncate_range
truncateOfLE 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike add	—	—
bijective_cast 📖	mathematical	—	Function.Bijective Path cast	—	Function.bijective_id
cast_coe 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike cast	—	—
cast_rfl_rfl 📖	mathematical	—	cast	—	—
cast_symm 📖	mathematical	—	cast symm	—	—
cast_trans 📖	mathematical	—	cast trans	—	—
coe_mk' 📖	mathematical	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	DFunLike.coe Path instFunLike ContinuousMap ContinuousMap.instFunLike	—	Real.instIsOrderedRing
coe_mk_mk 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	DFunLike.coe Path instFunLike	—	Real.instIsOrderedRing
coe_reparam 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	DFunLike.coe Path instFunLike reparam	—	Real.instIsOrderedRing
coe_toContinuousMap 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike toContinuousMap Path instFunLike	—	—
continuous 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Path instFunLike	—	ContinuousMap.continuous_toFun
continuousMapClass 📖	mathematical	—	ContinuousMapClass Path Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike	—	ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass
continuous_extend 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap ContinuousMap.instFunLike extend	—	Continuous.Icc_extend' instOrderTopologyReal continuous
continuous_symm 📖	mathematical	—	Continuous Path instTopologicalSpace symm	—	continuous_uncurry_iff symm_continuous_family Continuous.eval instContinuousEvalElemRealUnitInterval Continuous.fst continuous_id' Continuous.snd
continuous_trans 📖	mathematical	—	Continuous Path instTopologicalSpaceProd instTopologicalSpace trans	—	Continuous.path_trans Continuous.fst continuous_id' Continuous.snd
continuous_uncurry_extend_of_continuous_family 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry instHasUncurryPath	Function.hasUncurryInduction Function.hasUncurryBase DFunLike.coe ContinuousMap ContinuousMap.instFunLike extend	—	Continuous.comp zero_le_one Real.instZeroLEOneClass Continuous.prodMap continuous_id continuous_projIcc instOrderTopologyReal
continuous_uncurry_iff 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry instHasUncurryPath Path instTopologicalSpace	—	continuousMapClass continuous_induced_rng ContinuousMap.continuous_uncurry_of_continuous locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMap.continuous_of_continuous_uncurry ContinuousMapClass.map_continuous
exists_congr 📖	mathematical	—	cast	—	Function.Surjective.exists Function.Bijective.surjective bijective_cast
ext 📖	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike	—	—	Real.instIsOrderedRing
ext_iff 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike	—	ext
extend_apply 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Path Set.Elem unitInterval instFunLike	—	Set.IccExtend_of_mem
extend_cast 📖	mathematical	—	extend cast	—	—
extend_extends 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Path Set.Elem unitInterval instFunLike	—	extend_apply
extend_extends' 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Path Set.Elem unitInterval instFunLike	—	Set.IccExtend_val
extend_of_le_zero 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend	—	Set.left_mem_Icc Set.IccExtend_of_le_left source
extend_of_one_le 📖	mathematical	Real Real.instLE Real.instOne	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend	—	Set.right_mem_Icc Set.IccExtend_of_right_le target
extend_one 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instOne	—	Real.instZeroLEOneClass extend_apply target
extend_range 📖	mathematical	—	Set.range Real DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Set.Elem unitInterval Path instFunLike	—	Set.IccExtend_range
extend_symm 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend symm Real.instSub Real.instOne	—	extend_symm_apply
extend_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend symm Real.instSub Real.instOne	—	unitInterval.symm_projIcc
extend_trans_of_half_le 📖	mathematical	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend trans Real.instSub Real.instMul	—	Nat.instAtLeastTwoHAddOfNat sub_sub_cancel extend_symm_apply trans_symm extend_trans_of_le_half le_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.one_mul 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.mul_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add 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 Real.instIsStrictOrderedRing 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 IsStrictOrderedRing.toCharZero 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.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Ring.add_pf_add_gt
extend_trans_of_le_half 📖	mathematical	Real Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend trans Real.instMul	—	Nat.instAtLeastTwoHAddOfNat le_total extend_of_le_zero le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toCharZero Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one 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_neg extend_apply unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le trans_apply
extend_zero 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instZero	—	Real.instZeroLEOneClass extend_apply source
id_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne instFunLike id	—	Real.instIsOrderedRing
image_extend_of_subset 📖	mathematical	Set Real Set.instHasSubset unitInterval	Set.image DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Set.range Set.Elem Path instFunLike	—	HasSubset.Subset.antisymm Set.instAntisymmSubset Set.image_subset_range extend_range Set.range_subset_iff extend_extends'
instContinuousEvalElemRealUnitInterval 📖	mathematical	—	ContinuousEval Path Set.Elem Real unitInterval instFunLike instTopologicalSpace instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	ContinuousEval.of_continuous_forget ContinuousMap.instContinuousEvalOfLocallyCompactPair instLocallyCompactPairOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal continuousMapClass continuous_induced_dom
inv_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike inv	—	—
map_coe 📖	mathematical	Continuous	DFunLike.coe Path Set.Elem Real unitInterval instFunLike map	—	—
map_id 📖	mathematical	—	map continuous_id	—	ext continuous_id
map_map 📖	mathematical	Continuous	map Continuous.comp	—	ext Continuous.comp
map_symm 📖	mathematical	Continuous	symm map	—	—
map_trans 📖	mathematical	Continuous	map 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 map_coe
mul_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike mul	—	—
neg_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike neg	—	—
ofLine_extend 📖	mathematical	—	ofLine DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend extend_zero extend_one	—	ext extend_zero extend_one extend_apply Subtype.coe_eta
ofLine_mem 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace unitInterval Real.instZero Real.instOne	Set Set.instMembership Set.image DFunLike.coe Path Set.Elem instFunLike ofLine	—	—
pi_coe 📖	mathematical	—	DFunLike.coe Path Pi.topologicalSpace Set.Elem Real unitInterval instFunLike pi	—	—
prod_coe 📖	mathematical	—	DFunLike.coe Path instTopologicalSpaceProd Set.Elem Real unitInterval instFunLike prod	—	—
range_coe 📖	mathematical	—	Set.range ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path toContinuousMap instFunLike continuousMapClass setOf DFunLike.coe ContinuousMap.instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	—	Set.Subset.antisymm continuousMapClass Real.instIsOrderedRing Set.range_subset_iff source target
range_reparam 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	Set.range DFunLike.coe Path instFunLike reparam	—	Real.instIsOrderedRing Set.range_eq_univ zero_le_one' Real.instZeroLEOneClass Continuous.Icc_extend' instOrderTopologyReal intermediate_value_Icc LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology Continuous.continuousOn Set.right_mem_Icc Set.Icc.mk_one Set.left_mem_Icc Set.Icc.mk_zero Set.IccExtend_right Set.IccExtend_left Set.IccExtend_of_mem Set.range_comp Set.image_univ
refl_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike refl	—	—
refl_extend 📖	mathematical	—	extend refl ContinuousMap.const Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
refl_range 📖	mathematical	—	Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike refl Set Set.instSingletonSet	—	Set.range_const Nontrivial.to_nonempty unitInterval.instNontrivialElemReal
refl_reparam 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	reparam refl	—	Real.instIsOrderedRing ext
refl_symm 📖	mathematical	—	symm refl	—	—
refl_trans_refl 📖	mathematical	—	trans refl	—	ext one_div Real.instIsOrderedRing
reparam_id 📖	mathematical	—	reparam Set.Elem Real unitInterval continuous_id instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne	—	ext continuous_id Real.instIsOrderedRing
source 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	source'
source' 📖	mathematical	—	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toContinuousMap Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	—
source_mem_range 📖	mathematical	—	Set Set.instMembership Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike	—	Real.instIsOrderedRing source
symm_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike symm unitInterval.symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective Path symm	—	Function.bijective_iff_has_inverse symm_symm
symm_cast 📖	mathematical	—	symm cast	—	—
symm_continuous_family 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry instHasUncurryPath	symm	—	Continuous.comp Continuous.prodMap continuous_id unitInterval.continuous_symm
symm_range 📖	mathematical	—	Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike symm	—	Function.Surjective.range_comp Function.Involutive.surjective unitInterval.symm_involutive
symm_symm 📖	mathematical	—	symm	—	—
target 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval instFunLike Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	target'
target' 📖	mathematical	—	ContinuousMap.toFun Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toContinuousMap Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	—
target_mem_range 📖	mathematical	—	Set Set.instMembership Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike	—	Real.instIsOrderedRing target
trans_apply 📖	mathematical	—	DFunLike.coe Path 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 extend_apply
trans_cast 📖	mathematical	—	trans cast	—	—
trans_continuous_family 📖	mathematical	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Function.HasUncurry.uncurry instHasUncurryPath	trans	—	continuous_uncurry_extend_of_continuous_family Continuous.if_le OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.comp Nat.instAtLeastTwoHAddOfNat Continuous.prodMap continuous_id' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const continuous_subtype_val Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_snd Real.instZeroLEOneClass one_div mul_inv_cancel₀ IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing extend_apply target sub_self source
trans_pi_eq_pi_trans 📖	mathematical	—	trans Pi.topologicalSpace pi	—	ext
trans_prod_eq_prod_trans 📖	mathematical	—	trans instTopologicalSpaceProd prod	—	—
trans_range 📖	mathematical	—	Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike trans Set Set.instUnion	—	extend_range Set.image_univ Nat.instAtLeastTwoHAddOfNat Set.Iic_union_Ici Set.image_union Set.EqOn.image_eq extend_trans_of_le_half Set.mem_Iic extend_trans_of_half_le Set.mem_Ici Set.image_image Mathlib.Meta.NormNum.instAtLeastTwo 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.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Set.image_mul_left_Iic PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat image_extend_of_subset Set.image_mul_left_Ici Set.image_sub_const_Ici Real.instIsOrderedAddMonoid Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt
trans_symm 📖	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 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 unitInterval.coe_symm_eq 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 target unitInterval.symm_one source mul_sub sub_sub_eq_add_sub Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Linarith.add_neg lt_of_not_ge
truncate_const_continuous_family 📖	mathematical	—	Continuous Real Set.Elem unitInterval instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceSubtype Set Set.instMembership Function.HasUncurry.uncurry instHasUncurryPath DFunLike.coe ContinuousMap ContinuousMap.instFunLike extend Real.instMin truncate	—	Continuous.prodMk continuous_const continuous_id' Continuous.comp truncate_continuous_family
truncate_continuous_family 📖	mathematical	—	Continuous Real Set.Elem unitInterval instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpaceSubtype Set Set.instMembership DFunLike.coe Path ContinuousMap ContinuousMap.instFunLike extend Real.instMin instFunLike truncate	—	Continuous.comp continuous_extend Continuous.min OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.max continuous_subtype_val continuous_snd continuous_fst
truncate_one_one 📖	mathematical	—	truncate Real Real.instOne cast refl DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instMin extend_one	—	extend_one truncate_self
truncate_range 📖	mathematical	—	Set Set.instHasSubset Set.range Set.Elem Real unitInterval DFunLike.coe Path ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instMin instFunLike truncate	—	extend_range
truncate_self 📖	mathematical	—	truncate cast DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend refl Real.instMin	—	ext inf_of_le_right Real.instIsOrderedRing
truncate_zero_one 📖	mathematical	—	truncate Real Real.instZero Real.instOne cast DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instMin	—	ext cast_coe truncate.eq_1 max_eq_left min_eq_left extend_extends'
truncate_zero_zero 📖	mathematical	—	truncate Real Real.instZero cast refl DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike extend Real.instMin extend_zero	—	extend_zero truncate_self

Path.simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—

---

← Back to Index