PathConnected

📁 Source: Mathlib/Topology/Connected/PathConnected.lean

Statistics

Metric	Count
Definitions pathComponentZero, pathComponentZero, IsPathConnected, Joined, somePath, JoinedIn, somePath, PathConnectedSpace, somePath, pathComponentOne, pathComponentOne, ZerothHomotopy, inhabited, toConnectedComponents, instTopologicalSpaceZerothHomotopy, pathComponent, pathComponentIn, pathSetoid	18
Theorems pathComponentZero, coe_pathComponentZero, coe_pathComponentZero, pathConnectedSpace, isPathConnected_image, isPathConnected_preimage, joinedIn, add, exists_path_through_family, exists_path_through_family', image, image', inv, isConnected, joinedIn, mem_pathComponent, mul, neg, nonempty, preimage_coe, subset_pathComponent, subset_pathComponentIn, union, add, inv, listProd, listSum, mem_pathComponent, mul, neg, refl, trans, add, inv, joined, joined_subtype, map, map_continuousOn, mem, mono, mul, neg, ofLine, refl, somePath_mem, source_mem, target_mem, trans, connectedSpace, exists_path_through_family, exists_path_through_family', joined, nonempty, instPathConnectedSpace, instPathConnectedSpace, joinedIn, pathComponentOne, coe_pathComponentOne, coe_pathComponentOne, isPathConnected_iff, joinedIn_image, preimage_singleton_eq_pathComponent, toConnectedComponents_apply, toConnectedComponents_surjective, biUnion_connectedComponent_pathComponent_eq, instCompactSpaceZerothHomotopy, isPathConnected_iff, isPathConnected_iff_eq, isPathConnected_iff_pathConnectedSpace, isPathConnected_pathComponent, isPathConnected_pathComponentIn, isPathConnected_range, isPathConnected_singleton, isPathConnected_univ, joinedIn_iff_joined, joinedIn_univ, mem_pathComponentIn_self, mem_pathComponent_iff, mem_pathComponent_of_mem, mem_pathComponent_self, nonempty, pathComponentIn_congr, pathComponentIn_mono, pathComponentIn_nonempty_iff, pathComponentIn_subset, pathComponentIn_univ, pathComponent_congr, pathComponent_subset_component, pathComponent_symm, pathConnectedSpace_iff, pathConnectedSpace_iff_eq, pathConnectedSpace_iff_univ, pathConnectedSpace_iff_zerothHomotopy	93
Total	111

AddSubgroup

Definitions

Name	Category	Theorems
pathComponentZero 📖	CompOp	2 math math: Normal.pathComponentZero, coe_pathComponentZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pathComponentZero 📖	mathematical	—	SetLike.coe AddSubgroup instSetLike pathComponentZero pathComponent AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—

AddSubgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathComponentZero 📖	mathematical	—	AddSubgroup.Normal AddSubgroup.pathComponentZero	—	Continuous.add_const instSeparatelyContinuousAddOfContinuousAdd IsTopologicalAddGroup.toContinuousAdd Continuous.const_add ContinuousMapClass.map_continuous Path.continuousMapClass Real.instIsOrderedRing Path.source add_zero add_neg_cancel Path.target

AddSubmonoid

Definitions

Name	Category	Theorems
pathComponentZero 📖	CompOp	1 math math: coe_pathComponentZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pathComponentZero 📖	mathematical	—	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass instSetLike pathComponentZero pathComponent AddZero.toZero AddZeroClass.toAddZero	—	—

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathConnectedSpace 📖	mathematical	Continuous	PathConnectedSpace	—	pathConnectedSpace_iff_univ range_eq isPathConnected_range

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPathConnected_image 📖	mathematical	—	IsPathConnected Set.image DFunLike.coe Homeomorph EquivLike.toFunLike instEquivLike	—	Topology.IsInducing.isPathConnected_iff isInducing
isPathConnected_preimage 📖	mathematical	—	IsPathConnected Set.preimage DFunLike.coe Homeomorph EquivLike.toFunLike instEquivLike	—	image_symm isPathConnected_image

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
joinedIn 📖	mathematical	Inseparable Set Set.instMembership	JoinedIn	—	Specializes.joinedIn specializes

IsPathConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsPathConnected	IsPathConnected Set Set.add	—	Set.add_mem_add Set.forall_mem_image2 JoinedIn.add
exists_path_through_family 📖	mathematical	IsPathConnected Set Set.instMembership	Path Set Set.instHasSubset Set.range Set.Elem Real unitInterval DFunLike.coe Path.instFunLike Set.instMembership	—	Fin.snoc_last Path.exists_congr Fin.snoc_castSucc Path.refl_range Fin.isEmpty' Fin.snoc_apply_zero joinedIn Path.trans_range Set.range_subset_iff
exists_path_through_family' 📖	mathematical	IsPathConnected Set Set.instMembership	Path Set Set.instMembership DFunLike.coe Set.Elem Real unitInterval Path.instFunLike	—	exists_path_through_family Set.range_subset_iff
image 📖	mathematical	IsPathConnected Continuous	IsPathConnected Set.image	—	image' Continuous.continuousOn
image' 📖	mathematical	IsPathConnected ContinuousOn	IsPathConnected Set.image	—	Set.mem_image_of_mem ContinuousOn.mono Set.range_subset_iff JoinedIn.somePath_mem
inv 📖	mathematical	IsPathConnected	IsPathConnected Set Set.inv InvolutiveInv.toInv	—	Set.inv_mem_inv Set.image_inv_eq_inv inv_inv JoinedIn.map Set.mem_inv ContinuousInv.continuous_inv
isConnected 📖	mathematical	IsPathConnected	IsConnected	—	isConnected_iff_connectedSpace PathConnectedSpace.connectedSpace isPathConnected_iff_pathConnectedSpace
joinedIn 📖	mathematical	IsPathConnected Set Set.instMembership	JoinedIn	—	JoinedIn.trans JoinedIn.symm
mem_pathComponent 📖	mathematical	IsPathConnected Set Set.instMembership	Set Set.instMembership pathComponent	—	JoinedIn.joined joinedIn
mul 📖	mathematical	IsPathConnected	IsPathConnected Set Set.mul	—	Set.mul_mem_mul Set.forall_mem_image2 JoinedIn.mul
neg 📖	mathematical	IsPathConnected	IsPathConnected Set Set.neg InvolutiveNeg.toNeg	—	Set.neg_mem_neg Set.image_neg_eq_neg neg_neg JoinedIn.map Set.mem_neg ContinuousNeg.continuous_neg
nonempty 📖	mathematical	IsPathConnected	Set.Nonempty	—	isPathConnected_iff
preimage_coe 📖	mathematical	IsPathConnected Set Set.instHasSubset	IsPathConnected Set Set.instMembership instTopologicalSpaceSubtype Set.preimage	—	Topology.IsInducing.isPathConnected_iff Topology.IsInducing.subtypeVal Subtype.image_preimage_val Set.inter_eq_right
subset_pathComponent 📖	mathematical	IsPathConnected Set Set.instMembership	Set Set.instHasSubset pathComponent	—	mem_pathComponent
subset_pathComponentIn 📖	mathematical	IsPathConnected Set Set.instMembership Set.instHasSubset	Set Set.instHasSubset pathComponentIn	—	JoinedIn.mono joinedIn
union 📖	mathematical	IsPathConnected Set.Nonempty Set Set.instInter	IsPathConnected Set Set.instUnion	—	JoinedIn.mono joinedIn Set.subset_union_left Set.subset_union_right

Joined

Definitions

Name	Category	Theorems
somePath 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	Joined	—	—
inv 📖	mathematical	—	Joined	—	—
listProd 📖	mathematical	Joined	Joined MulOne.toMul MulOneClass.toMulOne MulOne.toOne	—	refl mul
listSum 📖	mathematical	Joined	Joined AddZero.toAdd AddZeroClass.toAddZero AddZero.toZero	—	refl add
mem_pathComponent 📖	mathematical	—	Set Set.instMembership pathComponent	—	trans
mul 📖	mathematical	—	Joined	—	—
neg 📖	mathematical	—	Joined	—	—
refl 📖	mathematical	—	Joined	—	—
trans 📖	mathematical	—	Joined	—	—

JoinedIn

Definitions

Name	Category	Theorems
somePath 📖	CompOp	1 math math: somePath_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	JoinedIn	JoinedIn Set Set.add	—	Set.add_mem_add somePath_mem
inv 📖	mathematical	JoinedIn	JoinedIn Set Set.inv InvolutiveInv.toInv	—	Set.inv_mem_inv somePath_mem
joined 📖	mathematical	JoinedIn	Joined	—	—
joined_subtype 📖	mathematical	JoinedIn	Joined Set Set.instMembership instTopologicalSpaceSubtype source_mem target_mem	—	source_mem target_mem somePath_mem ContinuousMapClass.map_continuous Path.continuousMapClass Real.instIsOrderedRing Path.source Path.target
map 📖	mathematical	JoinedIn Continuous	JoinedIn Set.image	—	map_continuousOn Continuous.continuousOn
map_continuousOn 📖	mathematical	JoinedIn ContinuousOn	JoinedIn Set.image	—	ContinuousOn.mono Set.range_subset_iff Set.mem_image_of_mem
mem 📖	mathematical	JoinedIn	Set Set.instMembership	—	Real.instIsOrderedRing Path.source Path.target
mono 📖	mathematical	JoinedIn Set Set.instHasSubset	JoinedIn	—	somePath_mem
mul 📖	mathematical	JoinedIn	JoinedIn Set Set.mul	—	Set.mul_mem_mul somePath_mem
neg 📖	mathematical	JoinedIn	JoinedIn Set Set.neg InvolutiveNeg.toNeg	—	Set.neg_mem_neg somePath_mem
ofLine 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace unitInterval Real.instZero Real.instOne Set Set.instHasSubset Set.image	JoinedIn	—	Path.ofLine_mem
refl 📖	mathematical	Set Set.instMembership	JoinedIn	—	—
somePath_mem 📖	mathematical	JoinedIn	Set Set.instMembership DFunLike.coe Path Set.Elem Real unitInterval Path.instFunLike somePath	—	—
source_mem 📖	mathematical	JoinedIn	Set Set.instMembership	—	mem
target_mem 📖	mathematical	JoinedIn	Set Set.instMembership	—	mem
trans 📖	mathematical	JoinedIn	JoinedIn	—	mem Joined.trans

PathConnectedSpace

Definitions

Name	Category	Theorems
somePath 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedSpace 📖	mathematical	—	ConnectedSpace	—	connectedSpace_iff_connectedComponent isPathConnected_iff_eq pathConnectedSpace_iff_univ Set.univ_subset_iff pathComponent_subset_component pathComponentIn_univ
exists_path_through_family 📖	mathematical	—	Path Set Set.instMembership Set.range Set.Elem Real unitInterval DFunLike.coe Path.instFunLike	—	pathConnectedSpace_iff_univ IsPathConnected.exists_path_through_family
exists_path_through_family' 📖	mathematical	—	Path DFunLike.coe Set.Elem Real unitInterval Path.instFunLike	—	pathConnectedSpace_iff_univ IsPathConnected.exists_path_through_family'
joined 📖	mathematical	—	Joined	—	—
nonempty 📖	—	—	—	—	—

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPathConnectedSpace 📖	mathematical	—	PathConnectedSpace instTopologicalSpaceQuotient	—	Function.Surjective.pathConnectedSpace mk'_surjective continuous_coinduced_rng

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPathConnectedSpace 📖	mathematical	—	PathConnectedSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	Continuous.comp' continuous_add IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Continuous.prodMk Continuous.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const continuous_subtype_val instIsOrderedRing sub_zero one_mul MulZeroClass.zero_mul add_zero sub_self zero_add

Specializes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
joinedIn 📖	mathematical	Specializes Set Set.instMembership	JoinedIn	—	Real.instIsOrderedRing IsClosed.continuous_piecewise_of_specializes isClosed_singleton Subtype.t1Space T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal continuous_const Set.piecewise_eq_of_notMem NeZero.one unitInterval.instNontrivialElemReal Set.piecewise_eq_of_mem

Subgroup

Definitions

Name	Category	Theorems
pathComponentOne 📖	CompOp	2 math math: coe_pathComponentOne, Normal.pathComponentOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pathComponentOne 📖	mathematical	—	SetLike.coe Subgroup instSetLike pathComponentOne pathComponent MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—

Subgroup.Normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathComponentOne 📖	mathematical	—	Subgroup.Normal Subgroup.pathComponentOne	—	Continuous.mul_const instSeparatelyContinuousMulOfContinuousMul IsTopologicalGroup.toContinuousMul Continuous.const_mul ContinuousMapClass.map_continuous Path.continuousMapClass Real.instIsOrderedRing Path.source mul_one mul_inv_cancel Path.target

Submonoid

Definitions

Name	Category	Theorems
pathComponentOne 📖	CompOp	1 math math: coe_pathComponentOne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pathComponentOne 📖	mathematical	—	SetLike.coe Submonoid Monoid.toMulOneClass instSetLike pathComponentOne pathComponent MulOne.toOne MulOneClass.toMulOne	—	—

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPathConnected_iff 📖	mathematical	Topology.IsInducing	IsPathConnected Set.image	—	joinedIn_image
joinedIn_image 📖	mathematical	Topology.IsInducing Set Set.instMembership	JoinedIn Set.image	—	Real.instIsOrderedRing specializes_iff Path.source specializes_refl Path.target continuous_iff ContinuousMapClass.map_continuous Path.continuousMapClass JoinedIn.trans Specializes.joinedIn JoinedIn.map continuous

ZerothHomotopy

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—
toConnectedComponents 📖	CompOp	3 math math: toConnectedComponents_apply, coe_connectedComponentsEquivZerothHomotopy_symm, toConnectedComponents_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_singleton_eq_pathComponent 📖	mathematical	—	Set.preimage pathSetoid Set Set.instSingletonSet pathComponent	—	Set.ext Set.mem_preimage Set.mem_singleton_iff mem_pathComponent_iff Quotient.eq
toConnectedComponents_apply 📖	mathematical	—	toConnectedComponents pathSetoid connectedComponentSetoid	—	—
toConnectedComponents_surjective 📖	mathematical	—	ZerothHomotopy ConnectedComponents toConnectedComponents	—	Quotient.map_surjective

(root)

Definitions

Name	Category	Theorems
IsPathConnected 📖	MathDef	41 math math: IsPathConnected.add, IsSimplyConnected.isPathConnected, Homeomorph.isPathConnected_preimage, isPathConnected_singleton, IsPathConnected.mul, Metric.isPathConnected_ball, isPathConnected_univ, isPathConnected_compl_singleton_of_one_lt_rank, Metric.isPathConnected_closedEBall, Convex.isPathConnected, Homeomorph.isPathConnected_image, IsPathConnected.inv, Set.Countable.isPathConnected_compl_of_one_lt_rank, IsPathConnected.image, pathConnected_subset_basis, isPathConnected_iff, isPathConnected_stdSimplex, IsPathConnected.neg, isPathConnected_pathComponent, isPathConnected_pathComponentIn, StarConvex.isPathConnected, Metric.isPathConnected_closedBall, isPathConnected_iff_eq, Unitary.isPathConnected_ball, isPathConnected_sphere, pathConnectedSpace_iff_univ, IsPathConnected.union, isOpen_isPathConnected_basis, isPathConnected_compl_of_isPathConnected_compl_zero, isPathConnected_iff_pathConnectedSpace, isPathConnected_compl_of_one_lt_codim, Metric.isPathConnected_eball, isPathConnected_range, LocPathConnectedSpace.path_connected_basis, IsPathConnected.preimage_coe, unitary.isPathConnected_ball, Submodule.isPathConnected, IsPathConnected.image', IsOpen.isConnected_iff_isPathConnected, Topology.IsInducing.isPathConnected_iff, isSimplyConnected_iff_exists_homotopy_refl_forall_mem
Joined 📖	MathDef	21 math math: Joined.refl, Joined.listProd, Joined.symm, connectedComponent_eq_iff_joined, Joined.trans, mem_pathComponent_iff, JoinedIn.joined, JoinedIn.joined_subtype, Joined.inv, joinedIn_univ, pathConnectedSpace_iff, Joined.listSum, unitary.joined, Unitary.joined, ContinuousMap.homotopic_const_iff, Joined.neg, Joined.mul, Joined.add, PathConnectedSpace.joined, joinedIn_iff_joined, selfAdjoint.joined_one_expUnitary
JoinedIn 📖	MathDef	19 math math: JoinedIn.inv, JoinedIn.map, JoinedIn.add, JoinedIn.mul, isPathConnected_iff, JoinedIn.neg, JoinedIn.symm, joinedIn_univ, JoinedIn.ofLine, IsPathConnected.joinedIn, Inseparable.joinedIn, Specializes.joinedIn, JoinedIn.map_continuousOn, JoinedIn.mono, JoinedIn.of_segment_subset, Topology.IsInducing.joinedIn_image, joinedIn_iff_joined, JoinedIn.trans, JoinedIn.refl
PathConnectedSpace 📖	CompData	25 math math: Quotient.instPathConnectedSpace, SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop, Complex.instPathConnectedSpaceUnits, Real.instPathConnectedSpace, instPathConnectedSpaceElemForallRealStdSimplexOfNonempty, SimplyConnectedSpace.instPathConnectedSpace, SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop₀, ContractibleSpace.instPathConnectedSpace, EuclideanHalfSpace.pathConnectedSpace, Function.Surjective.pathConnectedSpace, pathConnectedSpace_iff, simply_connected_iff_paths_homotopic, NormedSpace.instPathConnectedSpace, PathConnectedSpace.of_locPathConnectedSpace, pathConnectedSpace_iff_univ, IsTopologicalAddGroup.pathConnectedSpace, isPathConnected_iff_pathConnectedSpace, pathConnectedSpace_iff_zerothHomotopy, pathConnectedSpace_iff_connectedSpace, EuclideanQuadrant.pathConnectedSpace, AddCircle.pathConnectedSpace, simply_connected_iff_loops_nullhomotopic, simply_connected_iff_paths_homotopic', Convex.instPathConnectedSpace, pathConnectedSpace_iff_eq
ZerothHomotopy 📖	CompOp	8 math math: connectedComponentsEquivZerothHomotopy_symm_apply, instCompactSpaceZerothHomotopy, connectedComponentsEquivZerothHomotopy_apply, coe_connectedComponentsEquivZerothHomotopy_symm, ZerothHomotopy.toConnectedComponents_surjective, pathConnectedSpace_iff_zerothHomotopy, instFiniteZerothHomotopyOfCompactSpace, instDiscreteTopologyZerothHomotopy
instTopologicalSpaceZerothHomotopy 📖	CompOp	2 math math: instCompactSpaceZerothHomotopy, instDiscreteTopologyZerothHomotopy
pathComponent 📖	CompOp	27 math math: IsClopen.pathComponent, Unitary.mem_pathComponentOne_iff, OpenNormalSubgroup.pathComponentOne_carrier, Joined.mem_pathComponent, mem_pathComponent_iff, Subgroup.coe_pathComponentOne, pathComponent.nonempty, isPathConnected_pathComponent, IsPathConnected.subset_pathComponent, biUnion_connectedComponent_pathComponent_eq, AddSubmonoid.coe_pathComponentZero, pathComponent_congr, mem_pathComponent_self, ZerothHomotopy.preimage_singleton_eq_pathComponent, Submonoid.coe_pathComponentOne, pathComponent_subset_component, IsPathConnected.mem_pathComponent, AddSubgroup.coe_pathComponentZero, IsClosed.pathComponent, mem_pathComponent_of_mem, pathComponentIn_univ, OpenNormalAddSubgroup.pathComponentZero_carrier, pathComponent_eq_connectedComponent, unitary.mem_pathComponentOne_iff, pathConnectedSpace_iff_eq, IsOpen.pathComponent, pathComponent_symm
pathComponentIn 📖	CompOp	13 math math: locPathConnectedSpace_iff_pathComponentIn_mem_nhds, mem_pathComponentIn_self, IsOpen.pathComponentIn, IsPathConnected.subset_pathComponentIn, isPathConnected_pathComponentIn, isPathConnected_iff_eq, pathComponentIn_mono, pathComponentIn_subset, pathComponentIn_nonempty_iff, pathComponentIn_mem_nhds, pathComponentIn_univ, pathComponentIn_congr, locPathConnectedSpace_iff_isOpen_pathComponentIn
pathSetoid 📖	CompOp	5 math math: connectedComponentsEquivZerothHomotopy_symm_apply, connectedComponentSetoid_eq_pathSetoid, ZerothHomotopy.toConnectedComponents_apply, connectedComponentsEquivZerothHomotopy_apply, ZerothHomotopy.preimage_singleton_eq_pathComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion_connectedComponent_pathComponent_eq 📖	mathematical	—	Set.iUnion Set Set.instMembership connectedComponent pathComponent	—	pathComponent_subset_component connectedComponent_eq mem_pathComponent_self
instCompactSpaceZerothHomotopy 📖	mathematical	—	CompactSpace ZerothHomotopy instTopologicalSpaceZerothHomotopy	—	Quotient.compactSpace
isPathConnected_iff 📖	mathematical	—	IsPathConnected Set.Nonempty JoinedIn	—	IsPathConnected.joinedIn
isPathConnected_iff_eq 📖	mathematical	—	IsPathConnected Set Set.instMembership pathComponentIn	—	Set.ext JoinedIn.mem
isPathConnected_iff_pathConnectedSpace 📖	mathematical	—	IsPathConnected PathConnectedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	pathConnectedSpace_iff_univ Topology.IsInducing.isPathConnected_iff Topology.IsInducing.subtypeVal Set.image_univ Subtype.range_val_subtype Set.setOf_mem_eq
isPathConnected_pathComponent 📖	mathematical	—	IsPathConnected pathComponent	—	pathComponentIn_univ isPathConnected_pathComponentIn Set.mem_univ
isPathConnected_pathComponentIn 📖	mathematical	Set Set.instMembership	IsPathConnected pathComponentIn	—	mem_pathComponentIn_self Path.extend_zero Path.extend_extends' Real.instZeroLEOneClass
isPathConnected_range 📖	mathematical	Continuous	IsPathConnected Set.range	—	Set.image_univ IsPathConnected.image isPathConnected_univ
isPathConnected_singleton 📖	mathematical	—	IsPathConnected Set Set.instSingletonSet	—	JoinedIn.refl
isPathConnected_univ 📖	mathematical	—	IsPathConnected Set.univ	—	pathConnectedSpace_iff_univ
joinedIn_iff_joined 📖	mathematical	Set Set.instMembership	JoinedIn Joined Set Set.instMembership instTopologicalSpaceSubtype	—	JoinedIn.joined_subtype continuous_subtype_val Path.map_coe
joinedIn_univ 📖	mathematical	—	JoinedIn Set.univ Joined	—	—
mem_pathComponentIn_self 📖	mathematical	Set Set.instMembership	Set Set.instMembership pathComponentIn	—	JoinedIn.refl
mem_pathComponent_iff 📖	mathematical	—	Set Set.instMembership pathComponent Joined	—	—
mem_pathComponent_of_mem 📖	mathematical	—	Set Set.instMembership pathComponent	—	Joined.symm
mem_pathComponent_self 📖	mathematical	—	Set Set.instMembership pathComponent	—	Joined.refl
pathComponentIn_congr 📖	mathematical	Set Set.instMembership pathComponentIn	pathComponentIn	—	Set.ext JoinedIn.trans JoinedIn.symm
pathComponentIn_mono 📖	mathematical	Set Set.instHasSubset	Set Set.instHasSubset pathComponentIn	—	—
pathComponentIn_nonempty_iff 📖	mathematical	—	Set.Nonempty pathComponentIn Set Set.instMembership	—	Real.instIsOrderedRing Path.source mem_pathComponentIn_self
pathComponentIn_subset 📖	mathematical	—	Set Set.instHasSubset pathComponentIn	—	JoinedIn.target_mem
pathComponentIn_univ 📖	mathematical	—	pathComponentIn Set.univ pathComponent	—	—
pathComponent_congr 📖	mathematical	—	pathComponent	—	Set.ext pathComponent_symm Joined.symm Joined.trans
pathComponent_subset_component 📖	mathematical	—	Set Set.instHasSubset pathComponent connectedComponent	—	IsConnected.subset_connectedComponent isConnected_range unitInterval.instConnectedSpaceElemReal Path.continuous Real.instIsOrderedRing Path.source Path.target
pathComponent_symm 📖	mathematical	—	Set Set.instMembership pathComponent	—	mem_pathComponent_of_mem
pathConnectedSpace_iff 📖	mathematical	—	PathConnectedSpace Joined	—	—
pathConnectedSpace_iff_eq 📖	mathematical	—	PathConnectedSpace pathComponent Set.univ	—	pathComponentIn_univ
pathConnectedSpace_iff_univ 📖	mathematical	—	PathConnectedSpace IsPathConnected Set.univ	—	—
pathConnectedSpace_iff_zerothHomotopy 📖	mathematical	—	PathConnectedSpace ZerothHomotopy	—	nonempty_quotient_iff PathConnectedSpace.nonempty PathConnectedSpace.joined

pathComponent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty 📖	mathematical	—	Set.Nonempty pathComponent	—	mem_pathComponent_self

---

← Back to Index