LocallyConnected

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

Statistics

Metric	Count
Definitions LocallyConnectedSpace	1
Theorems toLocallyConnectedSpace, connectedComponentIn, locallyConnectedSpace, open_connected_basis, isOpen_isPreconnected, locallyConnectedSpace, connectedComponentIn_mem_nhds, instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace, instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace, isClopen_connectedComponent, isOpen_connectedComponent, locallyConnectedSpace_iff_connectedComponentIn_open, locallyConnectedSpace_iff_connected_basis, locallyConnectedSpace_iff_connected_subsets, locallyConnectedSpace_iff_hasBasis_isOpen_isConnected, locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected, locallyConnectedSpace_iff_subsets_isOpen_isConnected, locallyConnectedSpace_of_connected_bases	18
Total	19

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLocallyConnectedSpace 📖	mathematical	—	LocallyConnectedSpace	—	locallyConnectedSpace_iff_subsets_isOpen_isConnected Set.singleton_subset_iff mem_of_mem_nhds isOpen_discrete isConnected_singleton

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedComponentIn 📖	mathematical	IsOpen	connectedComponentIn	—	isOpen_iff_mem_nhds connectedComponentIn_eq connectedComponentIn_mem_nhds mem_nhds connectedComponentIn_subset
locallyConnectedSpace 📖	mathematical	IsOpen	LocallyConnectedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsOpenEmbedding.locallyConnectedSpace isOpenEmbedding_subtypeVal

LocallyConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
open_connected_basis 📖	mathematical	—	Filter.HasBasis Set nhds IsOpen Set.instMembership IsConnected	—	—

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_isPreconnected 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis setOf Set IsOpen IsPreconnected	—	of_hasBasis_nhds Filter.HasBasis.congr LocallyConnectedSpace.open_connected_basis

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyConnectedSpace 📖	mathematical	Topology.IsOpenEmbedding	LocallyConnectedSpace	—	locallyConnectedSpace_of_connected_bases Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.toIsInducing toIsEmbedding Filter.HasBasis.comap Filter.HasBasis.restrict_subset LocallyConnectedSpace.open_connected_basis IsOpen.mem_nhds isOpen_range Set.mem_range_self IsPreconnected.preimage_of_isOpenMap IsConnected.isPreconnected Topology.IsEmbedding.injective isOpenMap

(root)

Definitions

Name	Category	Theorems
LocallyConnectedSpace 📖	CompData	13 math math: locallyConnectedSpace_iff_connected_subsets, IsOpen.locallyConnectedSpace, Homeomorph.locallyConnectedSpace, locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected, DiscreteTopology.toLocallyConnectedSpace, locallyConnectedSpace_iff_connectedComponentIn_open, Topology.IsOpenEmbedding.locallyConnectedSpace, locallyConnectedSpace_iff_connected_basis, instLocallyConnectedSpace, locallyConnectedSpace_of_connected_bases, locallyConnectedSpace_iff_subsets_isOpen_isConnected, locallyConnectedSpace_iff_hasBasis_isOpen_isConnected, ChartedSpace.locallyConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedComponentIn_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	connectedComponentIn	—	Filter.HasBasis.mem_iff LocallyConnectedSpace.open_connected_basis mem_nhds_iff IsPreconnected.subset_connectedComponentIn IsConnected.isPreconnected
instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace 📖	mathematical	—	DiscreteTopology ConnectedComponents ConnectedComponents.instTopologicalSpace	—	discreteTopology_iff_isOpen_singleton ConnectedComponents.surjective_coe Topology.IsQuotientMap.isOpen_preimage ConnectedComponents.isQuotientMap_coe connectedComponents_preimage_singleton
instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace 📖	mathematical	—	Finite ConnectedComponents	—	finite_of_compact_of_discrete instCompactSpaceConnectedComponents instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace
isClopen_connectedComponent 📖	mathematical	—	IsClopen connectedComponent	—	isClosed_connectedComponent isOpen_connectedComponent
isOpen_connectedComponent 📖	mathematical	—	IsOpen connectedComponent	—	connectedComponentIn_univ IsOpen.connectedComponentIn isOpen_univ
locallyConnectedSpace_iff_connectedComponentIn_open 📖	mathematical	—	LocallyConnectedSpace IsOpen connectedComponentIn	—	IsOpen.connectedComponentIn locallyConnectedSpace_iff_subsets_isOpen_isConnected HasSubset.Subset.trans Set.instIsTransSubset connectedComponentIn_subset interior_subset isOpen_interior mem_interior_iff_mem_nhds mem_connectedComponentIn isConnected_connectedComponentIn_iff
locallyConnectedSpace_iff_connected_basis 📖	mathematical	—	LocallyConnectedSpace Filter.HasBasis Set nhds Filter Filter.instMembership IsPreconnected	—	locallyConnectedSpace_iff_connected_subsets Filter.hasBasis_self
locallyConnectedSpace_iff_connected_subsets 📖	mathematical	—	LocallyConnectedSpace Set Filter Filter.instMembership nhds IsPreconnected Set.instHasSubset	—	locallyConnectedSpace_iff_subsets_isOpen_isConnected IsOpen.mem_nhds IsConnected.isPreconnected locallyConnectedSpace_iff_connectedComponentIn_open isOpen_iff_mem_nhds connectedComponentIn_eq connectedComponentIn_subset Filter.mem_of_superset IsPreconnected.subset_connectedComponentIn mem_of_mem_nhds
locallyConnectedSpace_iff_hasBasis_isOpen_isConnected 📖	mathematical	—	LocallyConnectedSpace Filter.HasBasis Set nhds IsOpen Set.instMembership IsConnected	—	LocallyConnectedSpace.open_connected_basis
locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected 📖	mathematical	—	LocallyConnectedSpace TopologicalSpace.IsTopologicalBasis setOf Set IsOpen IsPreconnected	—	TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected Filter.HasBasis.congr TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
locallyConnectedSpace_iff_subsets_isOpen_isConnected 📖	mathematical	—	LocallyConnectedSpace Set Set.instHasSubset IsOpen Set.instMembership IsConnected	—	Filter.HasBasis.mem_iff mem_nhds_iff
locallyConnectedSpace_of_connected_bases 📖	mathematical	Filter.HasBasis nhds IsPreconnected	LocallyConnectedSpace	—	locallyConnectedSpace_iff_connected_basis Filter.HasBasis.to_hasBasis Filter.HasBasis.mem_of_mem subset_rfl Set.instReflSubset Filter.HasBasis.property_index Filter.HasBasis.set_index_subset

---

← Back to Index