Basic

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

Statistics

Metric	Count
Definitions `ConnectedSpace`, `IsPreconnected`, `PreconnectedSpace`, `connectedComponent`, `connectedComponentIn`	5
Theorems `toNonempty`, `toPreconnectedSpace`, `image_connectedComponentIn_subset`, `image_connectedComponent_subset`, `mapsTo_connectedComponent`, `mapsTo_connectedComponentIn`, `preconnectedSpace`, `connectedSpace`, `connectedSpace`, `biUnion_of_chain`, `biUnion_of_reflTransGen`, `closure`, `iUnion_of_chain`, `iUnion_of_reflTransGen`, `image`, `isPreconnected`, `nonempty`, `preimage_of_isClosedMap`, `preimage_of_isOpenMap`, `prod`, `subset_closure`, `subset_connectedComponent`, `union`, `isConnected`, `biUnion_of_chain`, `biUnion_of_reflTransGen`, `closure`, `connectedComponentIn`, `gt_of_ne`, `iUnion_of_chain`, `iUnion_of_reflTransGen`, `image`, `lt_of_ne`, `mapsTo_Ioi_or_Iio`, `preimage_of_isClosedMap`, `preimage_of_isOpenMap`, `prod`, `sUnion_directed`, `subset_closure`, `subset_connectedComponent`, `subset_connectedComponentIn`, `subset_left_of_subset_union`, `subset_of_closure_inter_subset`, `subset_or_subset`, `subset_right_of_subset_union`, `union`, `union'`, `isPreconnected`, `connectedComponent_eq_univ`, `isPreconnected_univ`, `preconnectedSpace`, `instConnectedSpace`, `isPreconnected`, `connectedSpace`, `preconnectedSpace`, `isPreconnected_image`, `connectedComponentIn_eq`, `connectedComponentIn_eq_empty`, `connectedComponentIn_eq_image`, `connectedComponentIn_mono`, `connectedComponentIn_nonempty_iff`, `connectedComponentIn_subset`, `connectedComponentIn_univ`, `connectedComponent_disjoint`, `connectedComponent_eq`, `connectedComponent_eq_iff_mem`, `connectedComponent_nonempty`, `connectedSpace_iff_connectedComponent`, `connectedSpace_iff_univ`, `instConnectedSpaceForall`, `instConnectedSpaceProd`, `instPreconnectedSpaceForall`, `instPreconnectedSpaceProd`, `irreducibleComponent_subset_connectedComponent`, `isClosed_connectedComponent`, `isConnected_connectedComponent`, `isConnected_connectedComponentIn_iff`, `isConnected_iff_connectedSpace`, `isConnected_range`, `isConnected_singleton`, `isConnected_univ`, `isConnected_univ_pi`, `isPreconnected_closed_iff`, `isPreconnected_connectedComponent`, `isPreconnected_connectedComponentIn`, `isPreconnected_empty`, `isPreconnected_iUnion`, `isPreconnected_iff_preconnectedSpace`, `isPreconnected_of_forall`, `isPreconnected_of_forall_pair`, `isPreconnected_range`, `isPreconnected_sUnion`, `isPreconnected_singleton`, `isPreconnected_univ_pi`, `mem_connectedComponent`, `mem_connectedComponentIn`, `preconnectedSpace_iff_connectedComponent`, `preconnectedSpace_iff_univ`	98
Total	103

ConnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNonempty` 📖	—	—	—	—	—
`toPreconnectedSpace` 📖	mathematical	—	`PreconnectedSpace`	—	—

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_connectedComponentIn_subset` 📖	mathematical	`Continuous` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.image` `connectedComponentIn`	—	`IsPreconnected.subset_connectedComponentIn` `IsPreconnected.image` `isPreconnected_connectedComponentIn` `continuousOn` `Set.mem_image_of_mem` `mem_connectedComponentIn` `Set.image_mono` `connectedComponentIn_subset`
`image_connectedComponent_subset` 📖	mathematical	`Continuous`	`Set` `Set.instHasSubset` `Set.image` `connectedComponent`	—	`IsConnected.subset_connectedComponent` `IsConnected.image` `isConnected_connectedComponent` `continuousOn` `Set.mem_image` `mem_connectedComponent`
`mapsTo_connectedComponent` 📖	mathematical	`Continuous`	`Set.MapsTo` `connectedComponent`	—	`Set.mapsTo_iff_image_subset` `image_connectedComponent_subset`
`mapsTo_connectedComponentIn` 📖	mathematical	`Continuous` `Set` `Set.instMembership`	`Set.MapsTo` `connectedComponentIn` `Set.image`	—	`Set.mapsTo_iff_image_subset` `image_connectedComponentIn_subset`

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preconnectedSpace` 📖	mathematical	`DenseRange` `Continuous`	`PreconnectedSpace`	—	`IsPreconnected.closure` `isPreconnected_range` `Dense.closure_eq`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedSpace` 📖	mathematical	`Continuous`	`ConnectedSpace`	—	`connectedSpace_iff_univ` `range_eq` `isConnected_range`

IrreducibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedSpace` 📖	mathematical	—	`ConnectedSpace`	—	`PreirreducibleSpace.preconnectedSpace` `toPreirreducibleSpace` `toNonempty`

IsConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_of_chain` 📖	mathematical	`Set.Nonempty` `IsConnected` `Set` `Set.instInter` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.iUnion` `Set.instMembership`	—	`Set.nonempty_biUnion` `Set.Nonempty.some_mem` `nonempty` `IsPreconnected.biUnion_of_chain` `isPreconnected`
`biUnion_of_reflTransGen` 📖	mathematical	`Set.Nonempty` `IsConnected` `Relation.ReflTransGen` `Set` `Set.instInter` `Set.instMembership`	`Set.iUnion`	—	`Set.nonempty_biUnion` `Set.Nonempty.some_mem` `nonempty` `IsPreconnected.biUnion_of_reflTransGen` `isPreconnected`
`closure` 📖	mathematical	`IsConnected`	`closure`	—	`subset_closure` `subset_closure` `Set.Subset.rfl`
`iUnion_of_chain` 📖	mathematical	`IsConnected` `Set.Nonempty` `Set` `Set.instInter` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.iUnion`	—	`iUnion_of_reflTransGen` `reflTransGen_of_succ`
`iUnion_of_reflTransGen` 📖	mathematical	`IsConnected` `Relation.ReflTransGen` `Set.Nonempty` `Set` `Set.instInter`	`Set.iUnion`	—	`Set.nonempty_iUnion` `nonempty` `IsPreconnected.iUnion_of_reflTransGen` `isPreconnected`
`image` 📖	mathematical	`IsConnected` `ContinuousOn`	`Set.image`	—	`Set.image_nonempty` `nonempty` `IsPreconnected.image` `isPreconnected`
`isPreconnected` 📖	mathematical	`IsConnected`	`IsPreconnected`	—	—
`nonempty` 📖	mathematical	`IsConnected`	`Set.Nonempty`	—	—
`preimage_of_isClosedMap` 📖	mathematical	`IsConnected` `IsClosedMap` `Set` `Set.instHasSubset` `Set.range`	`Set.preimage`	—	`Set.Nonempty.preimage'` `nonempty` `IsPreconnected.preimage_of_isClosedMap` `isPreconnected`
`preimage_of_isOpenMap` 📖	mathematical	`IsConnected` `IsOpenMap` `Set` `Set.instHasSubset` `Set.range`	`Set.preimage`	—	`Set.Nonempty.preimage'` `nonempty` `IsPreconnected.preimage_of_isOpenMap` `isPreconnected`
`prod` 📖	mathematical	`IsConnected`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.Nonempty.prod` `IsPreconnected.prod`
`subset_closure` 📖	—	`IsConnected` `Set` `Set.instHasSubset` `closure`	—	—	`Set.Nonempty.mono` `IsPreconnected.subset_closure`
`subset_connectedComponent` 📖	mathematical	`IsConnected` `Set` `Set.instMembership`	`Set.instHasSubset` `connectedComponent`	—	`IsPreconnected.subset_connectedComponent`
`union` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter` `IsConnected`	`Set.instUnion`	—	`Set.mem_union_left` `Set.mem_of_mem_inter_left` `IsPreconnected.union` `Set.mem_of_mem_inter_right` `isPreconnected`

IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConnected` 📖	mathematical	`IsIrreducible`	`IsConnected`	—	`nonempty` `IsPreirreducible.isPreconnected` `isPreirreducible`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_of_chain` 📖	mathematical	`IsPreconnected` `Set.Nonempty` `Set` `Set.instInter` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.iUnion` `Set.instMembership`	—	`Set.OrdConnected.out` `Set.Ico_subset_Icc_self` `LE.le.trans` `Order.le_succ` `Order.succ_le_of_lt` `biUnion_of_reflTransGen` `reflTransGen_of_succ` `Set.inter_comm`
`biUnion_of_reflTransGen` 📖	mathematical	`IsPreconnected` `Relation.ReflTransGen` `Set.Nonempty` `Set` `Set.instInter` `Set.instMembership`	`Set.iUnion`	—	`Set.singleton_subset_iff` `Set.mem_singleton` `Set.biUnion_singleton` `Set.insert_subset_iff` `Set.mem_insert_of_mem` `Set.mem_insert` `Set.biUnion_insert` `union'` `Set.Nonempty.mono` `Set.inter_comm` `Set.inter_subset_inter_right` `Set.subset_biUnion_of_mem` `isPreconnected_of_forall_pair` `Set.mem_iUnion₂` `Set.biUnion_subset_biUnion_left` `Set.mem_biUnion`
`closure` 📖	mathematical	`IsPreconnected`	`closure`	—	`subset_closure` `subset_closure` `Set.Subset.rfl`
`connectedComponentIn` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership`	`connectedComponentIn`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `connectedComponentIn_subset` `subset_connectedComponentIn` `subset_rfl` `Set.instReflSubset`
`gt_of_ne` 📖	—	`IsPreconnected` `ContinuousOn` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`mapsTo_Ioi_or_Iio` `not_forall₂_of_exists₂_not`
`iUnion_of_chain` 📖	mathematical	`IsPreconnected` `Set.Nonempty` `Set` `Set.instInter` `Order.succ` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.iUnion`	—	`iUnion_of_reflTransGen` `reflTransGen_of_succ`
`iUnion_of_reflTransGen` 📖	mathematical	`IsPreconnected` `Relation.ReflTransGen` `Set.Nonempty` `Set` `Set.instInter`	`Set.iUnion`	—	`Set.biUnion_univ` `biUnion_of_reflTransGen`
`image` 📖	mathematical	`IsPreconnected` `ContinuousOn`	`Set.image`	—	`continuousOn_iff'` `Set.subset_inter` `Set.preimage_union` `Set.image_subset_iff` `Set.Subset.rfl` `Set.subset_inter_iff` `Set.union_inter_distrib_right` `Set.inter_comm` `Set.inter_assoc` `Set.inter_left_comm` `Set.inter_self`
`lt_of_ne` 📖	—	`IsPreconnected` `ContinuousOn` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`mapsTo_Ioi_or_Iio` `not_forall₂_of_exists₂_not`
`mapsTo_Ioi_or_Iio` 📖	mathematical	`IsPreconnected` `ContinuousOn`	`Set.MapsTo` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Iio`	—	`subset_or_subset` `isOpen_Ioi` `instClosedIicTopology` `isOpen_Iio` `instClosedIciTopology` `image`
`preimage_of_isClosedMap` 📖	mathematical	`IsPreconnected` `IsClosedMap` `Set` `Set.instHasSubset` `Set.range`	`Set.preimage`	—	`isPreconnected_closed_iff` `Set.image_preimage_eq_of_subset` `Set.image_union` `Set.image_mono` `Set.image_preimage_inter` `Set.Nonempty.image` `Function.Injective.mem_set_image`
`preimage_of_isOpenMap` 📖	mathematical	`IsPreconnected` `IsOpenMap` `Set` `Set.instHasSubset` `Set.range`	`Set.preimage`	—	`Set.image_preimage_eq_of_subset` `Set.image_union` `Set.image_mono` `Set.image_preimage_inter` `Set.Nonempty.image` `Function.Injective.mem_set_image`
`prod` 📖	mathematical	`IsPreconnected`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`isPreconnected_of_forall_pair` `union` `image` `ContinuousOn.prodMk` `continuousOn_const` `continuousOn_id'` `Continuous.continuousOn` `Continuous.prodMk_left`
`sUnion_directed` 📖	mathematical	`DirectedOn` `Set` `Set.instHasSubset` `IsPreconnected`	`Set.sUnion`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_sUnion_of_mem` `Set.inter_subset_inter_left` `Set.Nonempty.mono`
`subset_closure` 📖	—	`IsPreconnected` `Set` `Set.instHasSubset` `closure`	—	—	`mem_closure_iff` `Set.Subset.trans`
`subset_connectedComponent` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership`	`Set.instHasSubset` `connectedComponent`	—	`Set.mem_sUnion_of_mem`
`subset_connectedComponentIn` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Set.instHasSubset`	`connectedComponentIn`	—	`Topology.IsInducing.isPreconnected_image` `Topology.IsInducing.subtypeVal` `Subtype.image_preimage_coe` `Set.inter_eq_right` `Set.mem_preimage` `subset_connectedComponent` `connectedComponentIn_eq_image` `Set.Subset.trans` `subset_refl` `Set.instReflSubset` `Set.image_mono`
`subset_left_of_subset_union` 📖	—	`IsOpen` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.instUnion` `Set.Nonempty` `Set.instInter` `IsPreconnected`	—	—	`Disjoint.subset_left_of_subset_union` `Set.not_disjoint_iff_nonempty_inter` `Set.disjoint_iff`
`subset_of_closure_inter_subset` 📖	—	`IsPreconnected` `IsOpen` `Set.Nonempty` `Set` `Set.instInter` `Set.instHasSubset` `closure`	—	—	`Set.mem_inter` `subset_left_of_subset_union` `IsClosed.isOpen_compl` `isClosed_closure` `Disjoint.mono_right` `Set.compl_subset_compl` `subset_closure` `disjoint_compl_right`
`subset_or_subset` 📖	—	`IsOpen` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.instUnion` `IsPreconnected`	—	—	`Set.eq_empty_or_nonempty` `Disjoint.subset_right_of_subset_union` `Set.disjoint_iff_inter_eq_empty` `Disjoint.subset_left_of_subset_union` `Set.disjoint_empty`
`subset_right_of_subset_union` 📖	—	`IsOpen` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.instUnion` `Set.Nonempty` `Set.instInter` `IsPreconnected`	—	—	`subset_left_of_subset_union` `Disjoint.symm` `Set.union_comm`
`union` 📖	mathematical	`Set` `Set.instMembership` `IsPreconnected`	`Set.instUnion`	—	`isPreconnected_sUnion` `Set.sUnion_pair`
`union'` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter` `IsPreconnected`	`Set.instUnion`	—	`union`

IsPreirreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreconnected` 📖	mathematical	`IsPreirreducible`	`IsPreconnected`	—	—

PreconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedComponent_eq_univ` 📖	mathematical	—	`connectedComponent` `Set.univ`	—	`preconnectedSpace_iff_connectedComponent`
`isPreconnected_univ` 📖	mathematical	—	`IsPreconnected` `Set.univ`	—	—

PreirreducibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preconnectedSpace` 📖	mathematical	—	`PreconnectedSpace`	—	`IsPreirreducible.isPreconnected` `isPreirreducible_univ`

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instConnectedSpace` 📖	mathematical	—	`ConnectedSpace` `instTopologicalSpaceQuotient`	—	`Function.Surjective.connectedSpace` `mk'_surjective` `continuous_coinduced_rng`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreconnected` 📖	mathematical	`Set.Subsingleton`	`IsPreconnected`	—	`induction_on` `isPreconnected_empty` `isPreconnected_singleton`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedSpace` 📖	mathematical	`IsConnected`	`ConnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`preconnectedSpace` `IsConnected.isPreconnected` `Set.Nonempty.to_subtype` `IsConnected.nonempty`
`preconnectedSpace` 📖	mathematical	`IsPreconnected`	`PreconnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Topology.IsInducing.isPreconnected_image` `Topology.IsInducing.subtypeVal` `Set.image_univ` `range_val`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreconnected_image` 📖	mathematical	`Topology.IsInducing`	`IsPreconnected` `Set.image`	—	`isOpen_iff` `Set.image_subset_iff` `Set.mem_image_of_mem` `IsPreconnected.image` `Continuous.continuousOn` `continuous`

(root)

Definitions

Name	Category	Theorems
`ConnectedSpace` 📖	CompData	14 math math: `OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace`, `IrreducibleSpace.connectedSpace`, `PathConnectedSpace.connectedSpace`, `connectedSpace_iff_connectedComponent`, `connectedSpace_iff_clopen`, `Subtype.connectedSpace`, `Quotient.instConnectedSpace`, `AddTorsor.connectedSpace`, `Function.Surjective.connectedSpace`, `instConnectedSpaceProd`, `pathConnectedSpace_iff_connectedSpace`, `connectedSpace_iff_univ`, `isConnected_iff_connectedSpace`, `unitInterval.instConnectedSpaceElemReal`
`IsPreconnected` 📖	MathDef	54 math math: `Metric.isPreconnected_ball`, `Sigma.isPreconnected_iff`, `Topology.IsInducing.isPreconnected_image`, `isPreconnected_uIoo`, `isPreconnected_iff_ordConnected`, `isPreconnected_Ici`, `isPreconnected_iff_preconnectedSpace`, `Homeomorph.isPreconnected_preimage`, `QuasiconvexOn.isPreconnected_preimage_subtype`, `isPreconnected_range`, `isPreconnected_Iic`, `locallyConnectedSpace_iff_connected_subsets`, `Metric.isPreconnected_closedEBall`, `isPreconnected_connectedComponentIn`, `isPreconnected_iff_subset_of_disjoint_closed`, `Set.OrdConnected.isPreconnected`, `isPreconnected_sphere`, `isPreconnected_of_forall_constant`, `isPreconnected_Icc`, `AffineSubspace.isPreconnected_setOf_wOppSide`, `QuasilinearOn.isPreconnected_preimage_subtype`, `setOf_isPreconnected_eq_of_ordered`, `isPreconnected_Ioi`, `Metric.isPreconnected_eball`, `isPreconnected_Ico`, `locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected`, `isPreconnected_connectedComponent`, `setOf_isPreconnected_subset_of_ordered`, `Real.convex_iff_isPreconnected`, `isPreconnected_singleton`, `isPreconnected_Ioc`, `isPreconnected_uIcc`, `isPreconnected_Ioo`, `TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected`, `AffineSubspace.isPreconnected_setOf_wSameSide`, `Homeomorph.isPreconnected_image`, `IsConnected.isPreconnected`, `QuasiconcaveOn.isPreconnected_preimage_subtype`, `locallyConnectedSpace_iff_connected_basis`, `isPreconnected_Iio`, `AffineSubspace.isPreconnected_setOf_sOppSide`, `IsPreirreducible.isPreconnected`, `isPreconnected_uIoc`, `isPreconnected_empty`, `Sum.isPreconnected_iff`, `preconnectedSpace_iff_univ`, `isPreconnected_iff_subset_of_fully_disjoint_closed`, `PreconnectedSpace.isPreconnected_univ`, `Metric.isPreconnected_closedBall`, `Set.Subsingleton.isPreconnected`, `isPreconnected_closed_iff`, `isPreconnected_iff_subset_of_disjoint`, `Convex.isPreconnected`, `AffineSubspace.isPreconnected_setOf_sSameSide`
`PreconnectedSpace` 📖	CompData	12 math math: `isPreconnected_iff_preconnectedSpace`, `ConnectedSpace.toPreconnectedSpace`, `DenseRange.preconnectedSpace`, `instPreconnectedSpaceProd`, `preconnectedSpace_of_forall_constant`, `IsDenseInducing.preconnectedSpace`, `preconnectedSpace_iff_connectedComponent`, `Subtype.preconnectedSpace`, `preconnectedSpace_iff_univ`, `ordered_connected_space`, `preconnectedSpace_iff_clopen`, `PreirreducibleSpace.preconnectedSpace`
`connectedComponent` 📖	CompOp	37 math math: `totallyDisconnectedSpace_iff_connectedComponent_singleton`, `Topology.IsQuotientMap.preimage_connectedComponent`, `ConnectedComponents.coe_eq_coe'`, `connectedComponent_eq_singleton`, `isConnected_connectedComponent`, `preimage_connectedComponent_connected`, `mem_connectedComponent`, `connectedSpace_iff_connectedComponent`, `connectedComponent_eq_iff_mem`, `Continuous.image_connectedComponent_subset`, `Continuous.mapsTo_connectedComponent`, `connectedComponents_preimage_singleton`, `connectedComponents_preimage_image`, `IsClopen.connectedComponent_subset`, `IsClopen.biUnion_connectedComponent_eq`, `connectedComponentIn_eq_image`, `isPreconnected_connectedComponent`, `connectedComponent_disjoint`, `isOpen_connectedComponent`, `isClopen_connectedComponent`, `pathComponent_subset_component`, `ConnectedComponents.coe_eq_coe`, `Topology.IsQuotientMap.image_connectedComponent`, `connectedComponent_nonempty`, `preconnectedSpace_iff_connectedComponent`, `Continuous.image_connectedComponent_eq_singleton`, `PreconnectedSpace.connectedComponent_eq_univ`, `DiscreteQuotient.proj_bot_eq`, `connectedComponent_eq_iInter_isClopen`, `isClosed_connectedComponent`, `irreducibleComponent_subset_connectedComponent`, `totallyDisconnectedSpace_iff_connectedComponent_subsingleton`, `connectedComponentIn_univ`, `connectedComponent_subset_iInter_isClopen`, `pathComponent_eq_connectedComponent`, `IsConnected.subset_connectedComponent`, `IsPreconnected.subset_connectedComponent`
`connectedComponentIn` 📖	CompOp	21 math math: `Subalgebra.spectrum_sUnion_connectedComponentIn`, `Continuous.image_connectedComponentIn_subset`, `connectedComponentIn_subset`, `mem_connectedComponentIn`, `isPreconnected_connectedComponentIn`, `connectedComponentIn_eq_image`, `connectedComponentIn_mono`, `IsPreconnected.connectedComponentIn`, `Subalgebra.spectrum_isBounded_connectedComponentIn`, `locallyConnectedSpace_iff_connectedComponentIn_open`, `connectedComponentIn_mem_nhds`, `connectedComponentIn_eq_empty`, `isConnected_connectedComponentIn_iff`, `connectedComponentIn_nonempty_iff`, `IsClopen.biUnion_connectedComponentIn`, `IsPreconnected.subset_connectedComponentIn`, `Continuous.mapsTo_connectedComponentIn`, `connectedComponentIn_univ`, `Homeomorph.image_connectedComponentIn`, `IsOpen.connectedComponentIn`, `Submodule.connectedComponentIn_eq_self_of_one_lt_codim`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedComponentIn_eq` 📖	—	`Set` `Set.instMembership` `connectedComponentIn`	—	—	`connectedComponentIn_nonempty_iff` `connectedComponentIn_eq_image` `connectedComponent_eq`
`connectedComponentIn_eq_empty` 📖	mathematical	`Set` `Set.instMembership`	`connectedComponentIn` `Set.instEmptyCollection`	—	—
`connectedComponentIn_eq_image` 📖	mathematical	`Set` `Set.instMembership`	`connectedComponentIn` `Set.image` `connectedComponent` `instTopologicalSpaceSubtype`	—	—
`connectedComponentIn_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`connectedComponentIn`	—	`connectedComponentIn_eq_image` `Set.image_comp` `Set.image_mono` `Continuous.image_connectedComponent_subset` `continuous_inclusion` `connectedComponentIn_eq_empty` `Set.empty_subset`
`connectedComponentIn_nonempty_iff` 📖	mathematical	—	`Set.Nonempty` `connectedComponentIn` `Set` `Set.instMembership`	—	`connectedComponentIn.eq_1`
`connectedComponentIn_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `connectedComponentIn`	—	`connectedComponentIn.eq_1` `Subtype.coe_preimage_self`
`connectedComponentIn_univ` 📖	mathematical	—	`connectedComponentIn` `Set.univ` `connectedComponent`	—	`subset_antisymm` `Set.instAntisymmSubset` `IsPreconnected.subset_connectedComponent` `isPreconnected_connectedComponentIn` `mem_connectedComponentIn` `IsPreconnected.subset_connectedComponentIn` `isPreconnected_connectedComponent` `mem_connectedComponent` `Set.subset_univ`
`connectedComponent_disjoint` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `connectedComponent`	—	`Set.disjoint_left` `connectedComponent_eq`
`connectedComponent_eq` 📖	—	`Set` `Set.instMembership` `connectedComponent`	—	—	`Set.eq_of_subset_of_subset` `IsConnected.subset_connectedComponent` `isConnected_connectedComponent` `Set.mem_of_mem_of_subset` `mem_connectedComponent`
`connectedComponent_eq_iff_mem` 📖	mathematical	—	`connectedComponent` `Set` `Set.instMembership`	—	`mem_connectedComponent` `connectedComponent_eq`
`connectedComponent_nonempty` 📖	mathematical	—	`Set.Nonempty` `connectedComponent`	—	`mem_connectedComponent`
`connectedSpace_iff_connectedComponent` 📖	mathematical	—	`ConnectedSpace` `connectedComponent` `Set.univ`	—	`Set.eq_univ_of_univ_subset` `IsPreconnected.subset_connectedComponent` `PreconnectedSpace.isPreconnected_univ` `Set.mem_univ` `isPreconnected_connectedComponent`
`connectedSpace_iff_univ` 📖	mathematical	—	`ConnectedSpace` `IsConnected` `Set.univ`	—	`Set.univ_nonempty` `ConnectedSpace.toNonempty` `PreconnectedSpace.isPreconnected_univ` `ConnectedSpace.toPreconnectedSpace`
`instConnectedSpaceForall` 📖	mathematical	`ConnectedSpace`	`Pi.topologicalSpace`	—	`instPreconnectedSpaceForall` `ConnectedSpace.toPreconnectedSpace` `ConnectedSpace.toNonempty`
`instConnectedSpaceProd` 📖	mathematical	—	`ConnectedSpace` `instTopologicalSpaceProd`	—	`instPreconnectedSpaceProd` `ConnectedSpace.toPreconnectedSpace` `ConnectedSpace.toNonempty`
`instPreconnectedSpaceForall` 📖	mathematical	`PreconnectedSpace`	`Pi.topologicalSpace`	—	`Set.pi_univ` `isPreconnected_univ_pi` `PreconnectedSpace.isPreconnected_univ`
`instPreconnectedSpaceProd` 📖	mathematical	—	`PreconnectedSpace` `instTopologicalSpaceProd`	—	`Set.univ_prod_univ` `IsPreconnected.prod` `PreconnectedSpace.isPreconnected_univ`
`irreducibleComponent_subset_connectedComponent` 📖	mathematical	—	`Set` `Set.instHasSubset` `irreducibleComponent` `connectedComponent`	—	`IsConnected.subset_connectedComponent` `IsIrreducible.isConnected` `isIrreducible_irreducibleComponent` `mem_irreducibleComponent`
`isClosed_connectedComponent` 📖	mathematical	—	`IsClosed` `connectedComponent`	—	`closure_subset_iff_isClosed` `IsConnected.subset_connectedComponent` `IsConnected.closure` `isConnected_connectedComponent` `subset_closure` `mem_connectedComponent`
`isConnected_connectedComponent` 📖	mathematical	—	`IsConnected` `connectedComponent`	—	`mem_connectedComponent` `isPreconnected_connectedComponent`
`isConnected_connectedComponentIn_iff` 📖	mathematical	—	`IsConnected` `connectedComponentIn` `Set` `Set.instMembership`	—	—
`isConnected_iff_connectedSpace` 📖	mathematical	—	`IsConnected` `ConnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Subtype.connectedSpace` `nonempty_subtype` `ConnectedSpace.toNonempty` `isPreconnected_iff_preconnectedSpace` `ConnectedSpace.toPreconnectedSpace`
`isConnected_range` 📖	mathematical	`Continuous`	`IsConnected` `Set.range`	—	`Set.range_nonempty` `ConnectedSpace.toNonempty` `isPreconnected_range` `ConnectedSpace.toPreconnectedSpace`
`isConnected_singleton` 📖	mathematical	—	`IsConnected` `Set` `Set.instSingletonSet`	—	`IsIrreducible.isConnected` `isIrreducible_singleton`
`isConnected_univ` 📖	mathematical	—	`IsConnected` `Set.univ`	—	`Set.univ_nonempty` `ConnectedSpace.toNonempty` `PreconnectedSpace.isPreconnected_univ` `ConnectedSpace.toPreconnectedSpace`
`isConnected_univ_pi` 📖	mathematical	—	`IsConnected` `Pi.topologicalSpace` `Set.pi` `Set.univ`	—	`Set.eval_image_univ_pi` `IsPreconnected.image` `Continuous.continuousOn` `continuous_apply` `isPreconnected_univ_pi`
`isPreconnected_closed_iff` 📖	mathematical	—	`IsPreconnected` `Set.Nonempty` `Set` `Set.instInter`	—	`Set.not_disjoint_iff_nonempty_inter` `Set.subset_compl_iff_disjoint_right` `Set.compl_inter` `IsClosed.isOpen_compl` `Set.Nonempty.ne_empty` `Set.compl_union` `Disjoint.inter_eq` `HasSubset.Subset.disjoint_compl_right` `IsOpen.isClosed_compl`
`isPreconnected_connectedComponent` 📖	mathematical	—	`IsPreconnected` `connectedComponent`	—	`isPreconnected_sUnion`
`isPreconnected_connectedComponentIn` 📖	mathematical	—	`IsPreconnected` `connectedComponentIn`	—	`connectedComponentIn.eq_1` `Topology.IsInducing.isPreconnected_image` `Topology.IsInducing.subtypeVal` `isPreconnected_connectedComponent` `isPreconnected_empty`
`isPreconnected_empty` 📖	mathematical	—	`IsPreconnected` `Set` `Set.instEmptyCollection`	—	`IsPreirreducible.isPreconnected` `isPreirreducible_empty`
`isPreconnected_iUnion` 📖	mathematical	`Set.Nonempty` `Set.iInter` `IsPreconnected`	`Set.iUnion`	—	`isPreconnected_sUnion` `Set.forall_mem_range`
`isPreconnected_iff_preconnectedSpace` 📖	mathematical	—	`IsPreconnected` `PreconnectedSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Subtype.preconnectedSpace` `Set.image_univ` `Subtype.range_coe_subtype` `IsPreconnected.image` `PreconnectedSpace.isPreconnected_univ` `Continuous.continuousOn` `continuous_subtype_val`
`isPreconnected_of_forall` 📖	—	`Set` `Set.instHasSubset` `Set.instMembership` `IsPreconnected`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.union_comm`
`isPreconnected_of_forall_pair` 📖	—	`Set` `Set.instHasSubset` `Set.instMembership` `IsPreconnected`	—	—	`Set.eq_empty_or_nonempty` `isPreconnected_empty` `isPreconnected_of_forall`
`isPreconnected_range` 📖	mathematical	`Continuous`	`IsPreconnected` `Set.range`	—	`IsPreconnected.image` `PreconnectedSpace.isPreconnected_univ` `Continuous.continuousOn` `Set.image_univ`
`isPreconnected_sUnion` 📖	mathematical	`Set` `Set.instMembership` `IsPreconnected`	`Set.sUnion`	—	`isPreconnected_of_forall` `Set.subset_sUnion_of_mem`
`isPreconnected_singleton` 📖	mathematical	—	`IsPreconnected` `Set` `Set.instSingletonSet`	—	`IsConnected.isPreconnected` `isConnected_singleton`
`isPreconnected_univ_pi` 📖	mathematical	`IsPreconnected`	`Pi.topologicalSpace` `Set.pi` `Set.univ`	—	`exists_finset_piecewise_mem_of_mem_nhds` `IsOpen.mem_nhds` `Finset.induction_on` `Finset.piecewise_empty` `Finset.piecewise_mem_set_pi` `Set.image_subset_iff` `Set.update_preimage_univ_pi` `IsPreconnected.image` `Continuous.continuousOn` `Continuous.update` `continuous_const` `continuous_id` `Set.mem_image_of_mem` `Finset.piecewise_insert` `Function.update_eq_self` `Set.Nonempty.mono` `Set.inter_subset_inter_left` `HasSubset.Subset.trans` `Set.instIsTransSubset`
`mem_connectedComponent` 📖	mathematical	—	`Set` `Set.instMembership` `connectedComponent`	—	`Set.mem_sUnion_of_mem` `Set.mem_singleton` `isPreconnected_singleton`
`mem_connectedComponentIn` 📖	mathematical	`Set` `Set.instMembership`	`connectedComponentIn`	—	`connectedComponentIn_eq_image`
`preconnectedSpace_iff_connectedComponent` 📖	mathematical	—	`PreconnectedSpace` `connectedComponent` `Set.univ`	—	`Set.eq_univ_of_univ_subset` `IsPreconnected.subset_connectedComponent` `PreconnectedSpace.isPreconnected_univ` `Set.mem_univ` `isEmpty_or_nonempty` `Set.univ_eq_empty_iff` `isPreconnected_empty` `isPreconnected_connectedComponent`
`preconnectedSpace_iff_univ` 📖	mathematical	—	`PreconnectedSpace` `IsPreconnected` `Set.univ`	—	`PreconnectedSpace.isPreconnected_univ`

---

← Back to Index