LocPathConnected

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

Statistics

Metric	Count
Definitions LocPathConnectedSpace	1
Theorems locPathConnectedSpace, pathComponent, pathComponent, isConnected_iff_isPathConnected, locPathConnectedSpace, pathComponent, pathComponentIn, coinduced, of_bases, path_connected_basis, of_locPathConnectedSpace, locPathConnectedSpace, locPathConnectedSpace, locPathConnectedSpace, locPathConnectedSpace, locPathConnectedSpace, locPathConnectedSpace, instDiscreteTopologyZerothHomotopy, instFiniteZerothHomotopyOfCompactSpace, instLocallyConnectedSpace, isOpen_isPathConnected_basis, locPathConnectedSpace_iff_isOpen_pathComponentIn, locPathConnectedSpace_iff_pathComponentIn_mem_nhds, pathComponentIn_mem_nhds, pathComponent_eq_connectedComponent, pathConnectedSpace_iff_connectedSpace, pathConnected_subset_basis	27
Total	28

AlexandrovDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace	—	LocPathConnectedSpace.of_bases nhds_basis_nhdsKer_singleton specializes_rfl JoinedIn.symm Specializes.joinedIn mem_nhdsKer_singleton specializes_refl

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathComponent 📖	mathematical	—	IsClopen pathComponent	—	IsClosed.pathComponent IsOpen.pathComponent

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pathComponent 📖	mathematical	—	IsClosed pathComponent	—	isOpen_compl_iff isOpen_iff_mem_nhds Filter.HasBasis.ex_mem LocPathConnectedSpace.path_connected_basis Filter.mp_mem Filter.univ_mem' Joined.trans JoinedIn.joined IsPathConnected.joinedIn mem_of_mem_nhds

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_iff_isPathConnected 📖	mathematical	IsOpen	IsConnected IsPathConnected	—	isConnected_iff_connectedSpace isPathConnected_iff_pathConnectedSpace pathConnectedSpace_iff_connectedSpace locPathConnectedSpace
locPathConnectedSpace 📖	mathematical	IsOpen	LocPathConnectedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsOpenEmbedding.locPathConnectedSpace isOpenEmbedding_subtypeVal
pathComponent 📖	mathematical	—	IsOpen pathComponent	—	pathComponentIn_univ pathComponentIn isOpen_univ
pathComponentIn 📖	mathematical	IsOpen	pathComponentIn	—	isOpen_iff_mem_nhds Filter.HasBasis.mem_iff LocPathConnectedSpace.path_connected_basis mem_nhds pathComponentIn_subset Filter.mem_of_superset IsPathConnected.subset_pathComponentIn mem_of_mem_nhds pathComponentIn_congr

LocPathConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced 📖	mathematical	—	LocPathConnectedSpace TopologicalSpace.coinduced	—	continuous_coinduced_rng locPathConnectedSpace_iff_isOpen_pathComponentIn isOpen_coinduced isOpen_iff_mem_nhds Set.preimage_mono pathComponentIn_subset mem_nhds_iff Set.image_subset_iff pathComponentIn_congr IsPathConnected.subset_pathComponentIn IsPathConnected.image isPathConnected_pathComponentIn mem_pathComponentIn_self HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono Set.image_preimage_subset IsOpen.pathComponentIn IsOpen.preimage
of_bases 📖	mathematical	Filter.HasBasis nhds IsPathConnected	LocPathConnectedSpace	—	Filter.hasBasis_self Filter.HasBasis.mem_iff Filter.HasBasis.mem_of_mem
path_connected_basis 📖	mathematical	—	Filter.HasBasis Set nhds Filter Filter.instMembership IsPathConnected	—	—

PathConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_locPathConnectedSpace 📖	mathematical	—	PathConnectedSpace	—	ConnectedSpace.toNonempty IsClopen.eq_univ IsClopen.pathComponent ConnectedSpace.toPreconnectedSpace

Quot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace instTopologicalSpaceQuot	—	Topology.IsQuotientMap.locPathConnectedSpace

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace instTopologicalSpaceQuotient	—	Topology.IsQuotientMap.locPathConnectedSpace isQuotientMap_quotient_mk'

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	LocPathConnectedSpace	instTopologicalSpaceSigma	—	locPathConnectedSpace_iff_pathComponentIn_mem_nhds mem_nhds_iff IsPathConnected.subset_pathComponentIn IsPathConnected.image isPathConnected_pathComponentIn continuous_sigmaMk mem_pathComponentIn_self HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono pathComponentIn_subset Set.image_preimage_subset isOpenMap_sigmaMk IsOpen.pathComponentIn IsOpen.preimage

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace instTopologicalSpaceSum	—	locPathConnectedSpace_iff_pathComponentIn_mem_nhds mem_nhds_iff IsPathConnected.subset_pathComponentIn IsPathConnected.image isPathConnected_pathComponentIn continuous_inl mem_pathComponentIn_self HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono pathComponentIn_subset Set.image_preimage_subset isOpenMap_inl IsOpen.pathComponentIn IsOpen.preimage continuous_inr isOpenMap_inr

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	Topology.IsOpenEmbedding	LocPathConnectedSpace	—	Topology.IsInducing.basis_nhds Topology.IsEmbedding.toIsInducing toIsEmbedding pathConnected_subset_basis isOpen_range Set.mem_range_self LocPathConnectedSpace.of_bases Topology.IsInducing.isPathConnected_iff Set.image_preimage_eq_of_subset

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locPathConnectedSpace 📖	mathematical	Topology.IsQuotientMap	LocPathConnectedSpace	—	LocPathConnectedSpace.coinduced eq_coinduced

(root)

Definitions

Name	Category	Theorems
LocPathConnectedSpace 📖	CompData	20 math math: ChartedSpace.locPathConnectedSpace, LocPathConnectedSpace.coinduced, Quot.locPathConnectedSpace, UpperHalfPlane.instLocPathConnectedSpace, locPathConnectedSpace_iff_pathComponentIn_mem_nhds, Unitary.instLocPathConnectedSpace, Quotient.locPathConnectedSpace, LocallyConvexSpace.toLocPathConnectedSpace, AlexandrovDiscrete.locPathConnectedSpace, Topology.IsOpenEmbedding.locPathConnectedSpace, Convex.locPathConnectedSpace, instLocPathConnectedSpaceEuclideanHalfSpace, IsOpen.locPathConnectedSpace, instLocPathConnectedSpace, Sum.locPathConnectedSpace, LocPathConnectedSpace.of_bases, DeltaGeneratedSpace.instLocPathConnectedSpace, Topology.IsQuotientMap.locPathConnectedSpace, locPathConnectedSpace_iff_isOpen_pathComponentIn, instLocPathConnectedSpaceEuclideanQuadrant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDiscreteTopologyZerothHomotopy 📖	mathematical	—	DiscreteTopology ZerothHomotopy instTopologicalSpaceZerothHomotopy	—	discreteTopology_iff_isOpen_singleton Quotient.mk_surjective Topology.IsQuotientMap.isOpen_preimage isQuotientMap_quotient_mk'
instFiniteZerothHomotopyOfCompactSpace 📖	mathematical	—	Finite ZerothHomotopy	—	finite_of_compact_of_discrete instCompactSpaceZerothHomotopy instDiscreteTopologyZerothHomotopy
instLocallyConnectedSpace 📖	mathematical	—	LocallyConnectedSpace	—	Filter.HasBasis.mem_iff' IsPathConnected.isConnected mem_nhds_iff isOpen_isPathConnected_basis
isOpen_isPathConnected_basis 📖	mathematical	—	Filter.HasBasis Set nhds IsOpen Set.instMembership IsPathConnected	—	mem_nhds_iff IsOpen.pathComponentIn mem_pathComponentIn_self isPathConnected_pathComponentIn HasSubset.Subset.trans Set.instIsTransSubset pathComponentIn_subset
locPathConnectedSpace_iff_isOpen_pathComponentIn 📖	mathematical	—	LocPathConnectedSpace IsOpen pathComponentIn	—	IsOpen.pathComponentIn mem_nhds_iff IsOpen.mem_nhds mem_pathComponentIn_self isPathConnected_pathComponentIn HasSubset.Subset.trans Set.instIsTransSubset pathComponentIn_subset Filter.mem_of_superset
locPathConnectedSpace_iff_pathComponentIn_mem_nhds 📖	mathematical	—	LocPathConnectedSpace Set Filter Filter.instMembership nhds pathComponentIn	—	locPathConnectedSpace_iff_isOpen_pathComponentIn IsOpen.mem_nhds mem_pathComponentIn_self isOpen_iff_mem_nhds pathComponentIn_congr pathComponentIn_subset
pathComponentIn_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	pathComponentIn	—	mem_nhds_iff pathComponentIn_mono IsOpen.pathComponentIn mem_pathComponentIn_self
pathComponent_eq_connectedComponent 📖	mathematical	—	pathComponent connectedComponent	—	HasSubset.Subset.antisymm Set.instAntisymmSubset pathComponent_subset_component IsClopen.connectedComponent_subset IsClopen.pathComponent mem_pathComponent_self
pathConnectedSpace_iff_connectedSpace 📖	mathematical	—	PathConnectedSpace ConnectedSpace	—	PathConnectedSpace.connectedSpace PathConnectedSpace.of_locPathConnectedSpace
pathConnected_subset_basis 📖	mathematical	IsOpen Set Set.instMembership	Filter.HasBasis nhds Filter Filter.instMembership IsPathConnected Set.instHasSubset	—	Filter.HasBasis.hasBasis_self_subset LocPathConnectedSpace.path_connected_basis IsOpen.mem_nhds

---

← Back to Index