Path

📁 Source: Mathlib/Topology/UniformSpace/Path.lean

Statistics

Metric	Count
Definitions Path, Path, Path, Path, Path, Path, instUniformSpace, Path, Path, Path	10
Theorems uniformityPath, hasBasis_uniformity, instCompleteSpace, isUniformEmbedding_coe, uniformContinuous, uniformContinuous_extend, uniformContinuous_extend_left, uniformContinuous_symm, uniformContinuous_trans	9
Total	19

CategoryTheory.SimplicialThickening

Definitions

Name	Category	Theorems
Path 📖	CompData	—

ExistsAndEq

Definitions

Name	Category	Theorems
Path 📖	CompOp	—

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uniformityPath 📖	mathematical	Filter.HasBasis uniformity	Path UniformSpace.toTopologicalSpace Path.instUniformSpace setOf	—	comap compactConvergenceUniformity_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal

MvPFunctor.M

Definitions

Name	Category	Theorems
Path 📖	CompData	—

NFA

Definitions

Name	Category	Theorems
Path 📖	CompData	2 math math: accepts_iff_exists_path, mem_evalFrom_iff_nonempty_path

PFunctor.Approx

Definitions

Name	Category	Theorems
Path 📖	CompOp	—

Path

Definitions

Name	Category	Theorems
instUniformSpace 📖	CompOp	7 math math: uniformContinuous_symm, uniformContinuous_extend_left, isUniformEmbedding_coe, uniformContinuous_trans, hasBasis_uniformity, instCompleteSpace, Filter.HasBasis.uniformityPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_uniformity 📖	mathematical	—	Filter.HasBasis Path UniformSpace.toTopologicalSpace Set uniformity instUniformSpace Filter Filter.instMembership setOf	—	Filter.HasBasis.uniformityPath Filter.basis_sets
instCompleteSpace 📖	mathematical	—	CompleteSpace Path UniformSpace.toTopologicalSpace instUniformSpace	—	IsUniformInducing.completeSpace continuousMapClass IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe Real.instIsOrderedRing range_coe Function.update_self Function.update_of_ne NeZero.one unitInterval.instNontrivialElemReal ContinuousMap.isComplete_setOf_eqOn ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
isUniformEmbedding_coe 📖	mathematical	—	IsUniformEmbedding Path UniformSpace.toTopologicalSpace ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instUniformSpace ContinuousMap.compactConvergenceUniformSpace toContinuousMap instFunLike continuousMapClass	—	continuousMapClass ContinuousMap.coe_injective'
uniformContinuous 📖	mathematical	—	UniformContinuous Set.Elem Real unitInterval instUniformSpaceSubtype Set Set.instMembership PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Path UniformSpace.toTopologicalSpace instFunLike	—	CompactSpace.uniformContinuous_of_continuous compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMapClass.map_continuous continuousMapClass
uniformContinuous_extend 📖	mathematical	—	UniformContinuous Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace ContinuousMap.instFunLike extend	—	UniformContinuous.comp uniformContinuous LipschitzWith.uniformContinuous LipschitzWith.projIcc
uniformContinuous_extend_left 📖	mathematical	—	UniformContinuous Path UniformSpace.toTopologicalSpace ContinuousMap Real PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instUniformSpace ContinuousMap.compactConvergenceUniformSpace extend	—	UniformContinuous.comp instOrderTopologyReal ZeroLEOneClass.factZeroLeOne Real.instZeroLEOneClass ContinuousMap.uniformContinuous_comp_left IsUniformInducing.uniformContinuous continuousMapClass IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coe
uniformContinuous_symm 📖	mathematical	—	UniformContinuous Path UniformSpace.toTopologicalSpace instUniformSpace symm	—	Filter.HasBasis.uniformContinuous_iff hasBasis_uniformity
uniformContinuous_trans 📖	mathematical	—	UniformContinuous Path UniformSpace.toTopologicalSpace instUniformSpaceProd instUniformSpace trans	—	Filter.HasBasis.uniformContinuous_iff Filter.HasBasis.uniformity_prod hasBasis_uniformity Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_div unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le trans_apply

SSet

Definitions

Name	Category	Theorems
Path 📖	CompOp	4 math math: StrictSegal.spineInjective, StrictSegal.spineToSimplex_spine, IsStrictSegal.segal, StrictSegal.spine_spineToSimplex

SSet.Truncated

Definitions

Name	Category	Theorems
Path 📖	CompOp	8 math math: StrictSegal.spine_spineToSimplex, StrictSegal.spineToSimplex_spine, StrictSegal.spineInjective, IsStrictSegal.spine_bijective, IsStrictSegal.segal, liftOfStrictSegal.spineEquiv_f₂_arrow_one, spine_injective, liftOfStrictSegal.spineEquiv_f₂_arrow_zero

SimpleGraph

Definitions

Name	Category	Theorems
Path 📖	CompOp	2 math math: Path.mapEmbedding_injective, Path.map_injective

(root)

Definitions

Name	Category	Theorems
Path 📖	CompData	87 math math: FundamentalGroupoid.eqToHom_eq, Path.subpath_self, IsPathConnected.exists_path_through_family', Path.continuousMapClass, Path.symm_bijective, Path.bijective_cast, Path.extend_extends, selfAdjoint.expUnitaryPathToOne_apply, Path.range_subpath_of_ge, Path.uniformContinuous_symm, Path.pi_coe, Path.ext_iff, ContinuousMap.Homotopy.evalAt_eq, Path.Homotopic.Quotient.mk'_eq_mk, Path.continuous_symm, Path.toHomotopyConst_apply, Path.extend_apply, Path.uniformContinuous_extend_left, Path.cast_coe, Path.ofLine_mem, Path.instSubsingletonPUnitUnit, Path.continuous_delayReflRight, Path.Homotopy.hcomp_apply, Path.continuous_delayReflLeft, Path.instContinuousEvalElemRealUnitInterval, Path.Homotopy.eval_apply, IsPathConnected.exists_path_through_family, Path.mul_apply, ContinuousMap.Homotopy.evalAt_apply, Path.uniformContinuous, Path.image_extend_of_subset, Path.extend_range, Path.isUniformEmbedding_coe, Path.range_subpath, Path.symm_apply, Path.uniformContinuous_trans, Path.inv_apply, Path.refl_apply, Path.range_segment, Path.continuous_uncurry_iff, Path.prod_coe, Manifold.riemannianEDist_def, GenLoop.toLoop_apply_coe, Path.range_reparam, Path.continuous, Path.source_mem_range, Path.neg_apply, Path.target_mem_range, PathConnectedSpace.exists_path_through_family, Path.trans_apply, Path.hasBasis_uniformity, Path.trans_range, Path.symm_subpath, Path.continuous_trans, PathConnectedSpace.exists_path_through_family', Path.coe_mk_mk, Path.range_coe, Path.add_apply, Path.map_coe, Path.subpath_continuous_family, JoinedIn.somePath_mem, Path.refl_range, Path.id_apply, Path.source, Path.coe_toContinuousMap, Path.Homotopic.Quotient.mk''_eq_mk, Path.extend_extends', Path.instCompleteSpace, Path.truncate_continuous_family, Filter.HasBasis.uniformityPath, Path.target, Path.subpath_zero_one, FundamentalGroupoid.id_eq_path_refl, Path.range_subpath_of_le, Path.segment_apply, Path.coe_reparam, Path.coe_mk', Path.Homotopy.refl_apply, Path.symm_range, Path.Homotopic.instIsEquiv, Unitary.path_apply, Path.truncate_range, Path.Homotopic.Quotient.mk_surjective, Path.Homotopic.concat_subpath, Path.Homotopic.equivalence, ContinuousMap.Homotopy.eq_diag_path, IsCoveringMap.liftPath_trans

---

← Back to Index