Clopen

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

Statistics

Metric	Count
Definitions `instCoeTC`, `instInhabited`, `instTopologicalSpace`, `mk`, `connectedComponentSetoid`	5
Theorems `coe_eq_coe`, `coe_eq_coe'`, `coe_ne_coe`, `continuous_coe`, `isQuotientMap_coe`, `range_coe`, `surjective_coe`, `exists_lift_sigma`, `biUnion_connectedComponentIn`, `biUnion_connectedComponent_eq`, `connectedComponent_subset`, `eq_univ`, `induction₂`, `induction₂'`, `subset_isClopen`, `induction₂`, `induction₂'`, `isConnected_iff`, `isPreconnected_iff`, `isConnected_iff`, `isPreconnected_iff`, `image_connectedComponent`, `preimage_connectedComponent`, `connectedComponent_subset_iInter_isClopen`, `connectedComponents_preimage_image`, `connectedComponents_preimage_singleton`, `connectedSpace_iff_clopen`, `disjoint_or_subset_of_isClopen`, `frontier_eq_empty_iff`, `instCompactSpaceConnectedComponents`, `isClopen_iff`, `isClopen_preimage_val`, `isConnected_iff_sUnion_disjoint_open`, `isPreconnected_iff_subset_of_disjoint`, `isPreconnected_iff_subset_of_disjoint_closed`, `isPreconnected_iff_subset_of_fully_disjoint_closed`, `isPreconnected_of_forall_constant`, `nonempty_frontier_iff`, `nonempty_inter`, `preconnectedSpace_iff_clopen`, `preconnectedSpace_of_forall_constant`, `preimage_connectedComponent_connected`, `subsingleton_of_disjoint_isClopen`, `subsingleton_of_disjoint_isClosed_iUnion_eq_univ`, `subsingleton_of_disjoint_isOpen_iUnion_eq_univ`	45
Total	50

ConnectedComponents

Definitions

Name	Category	Theorems
`instCoeTC` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instTopologicalSpace` 📖	CompOp	8 math math: `instCompactSpaceConnectedComponents`, `continuous_coe`, `Continuous.connectedComponentsMap_continuous`, `t2`, `isQuotientMap_coe`, `Continuous.connectedComponentsLift_continuous`, `instDiscreteTopologyConnectedComponentsOfLocallyConnectedSpace`, `totallyDisconnectedSpace`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_eq_coe` 📖	mathematical	—	`connectedComponent`	—	`Quotient.eq''`
`coe_eq_coe'` 📖	mathematical	—	`Set` `Set.instMembership` `connectedComponent`	—	`coe_eq_coe` `connectedComponent_eq_iff_mem`
`coe_ne_coe` 📖	—	—	—	—	`Iff.not` `coe_eq_coe`
`continuous_coe` 📖	mathematical	—	`Continuous` `ConnectedComponents` `instTopologicalSpace`	—	`Topology.IsQuotientMap.continuous` `isQuotientMap_coe`
`isQuotientMap_coe` 📖	mathematical	—	`Topology.IsQuotientMap` `ConnectedComponents` `instTopologicalSpace`	—	—
`range_coe` 📖	mathematical	—	`Set.range` `ConnectedComponents` `Set.univ`	—	`Function.Surjective.range_eq` `surjective_coe`
`surjective_coe` 📖	mathematical	—	`ConnectedComponents`	—	`Quot.mk_surjective`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lift_sigma` 📖	—	`Continuous` `instTopologicalSpaceSigma`	—	—	`Sigma.isConnected_iff` `isConnected_range` `Eq.trans_subset` `Set.image_subset_range` `Set.range_subset_range_iff_exists_comp` `Topology.IsEmbedding.continuous_iff` `Topology.IsEmbedding.sigmaMk`

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_connectedComponentIn` 📖	mathematical	`IsClopen` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.preimage` `Set.instHasSubset`	`Set.iUnion` `connectedComponentIn`	—	`biUnion_connectedComponent_eq` `Subtype.image_preimage_coe` `Set.inter_eq_right` `Set.iUnion_congr_Prop` `Set.iUnion_coe_set` `Set.image_val_iUnion` `le_antisymm` `Set.iUnion_subset` `le_rfl` `Set.subset_iUnion₂_of_subset`
`biUnion_connectedComponent_eq` 📖	mathematical	`IsClopen`	`Set.iUnion` `Set` `Set.instMembership` `connectedComponent`	—	`Set.Subset.antisymm` `Set.iUnion₂_subset` `connectedComponent_subset` `Set.mem_iUnion₂_of_mem` `mem_connectedComponent`
`connectedComponent_subset` 📖	mathematical	`IsClopen` `Set` `Set.instMembership`	`Set.instHasSubset` `connectedComponent`	—	`IsPreconnected.subset_isClopen` `isPreconnected_connectedComponent` `mem_connectedComponent`
`eq_univ` 📖	mathematical	`IsClopen` `Set.Nonempty`	`Set.univ`	—	`isClopen_iff` `Set.Nonempty.ne_empty`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction₂` 📖	—	`IsPreconnected` `Filter.Eventually` `nhdsWithin` `Set` `Set.instMembership`	—	—	`induction₂'` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'`
`induction₂'` 📖	—	`IsPreconnected` `Filter.Eventually` `nhdsWithin` `Set` `Set.instMembership`	—	—	`Subtype.preconnectedSpace` `PreconnectedSpace.induction₂'` `nhdsWithin_eq_map_subtype_coe`
`subset_isClopen` 📖	mathematical	`IsPreconnected` `IsClopen` `Set.Nonempty` `Set` `Set.instInter`	`Set.instHasSubset`	—	`subset_left_of_subset_union` `IsClopen.isOpen` `IsClopen.compl` `disjoint_compl_right` `Set.union_compl_self`

PreconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction₂` 📖	—	`Filter.Eventually` `nhds` `Transitive` `Symmetric`	—	—	`induction₂'` `Filter.mp_mem` `Filter.univ_mem'`
`induction₂'` 📖	—	`Filter.Eventually` `nhds` `Transitive`	—	—	`isClosed_iff_nhds` `isOpen_iff_mem_nhds` `Filter.mp_mem` `Filter.univ_mem'` `mem_of_mem_nhds` `IsClopen.eq_univ`

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConnected_iff` 📖	mathematical	—	`IsConnected` `instTopologicalSpaceSigma` `Set.image`	—	`IsConnected.nonempty` `IsPreconnected.subset_isClopen` `IsConnected.isPreconnected` `isClopen_range_sigmaMk` `IsConnected.preimage_of_isOpenMap` `sigma_mk_injective` `isOpenMap_sigmaMk` `Set.image_preimage_eq_of_subset` `IsConnected.image` `Continuous.continuousOn` `continuous_sigmaMk`
`isPreconnected_iff` 📖	mathematical	—	`IsPreconnected` `instTopologicalSpaceSigma` `Set.image`	—	`Set.eq_empty_or_nonempty` `isPreconnected_empty` `Set.image_empty` `isConnected_iff` `IsConnected.isPreconnected` `IsPreconnected.image` `Continuous.continuousOn` `continuous_sigmaMk`

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isConnected_iff` 📖	mathematical	—	`IsConnected` `instTopologicalSpaceSum` `Set.image`	—	`IsConnected.nonempty` `IsPreconnected.subset_isClopen` `IsConnected.isPreconnected` `isClopen_range_inl` `IsConnected.preimage_of_isOpenMap` `inl_injective` `isOpenMap_inl` `Set.image_preimage_eq_of_subset` `isClopen_range_inr` `inr_injective` `isOpenMap_inr` `IsConnected.image` `Continuous.continuousOn` `continuous_inl` `continuous_inr`
`isPreconnected_iff` 📖	mathematical	—	`IsPreconnected` `instTopologicalSpaceSum` `Set.image`	—	`Set.eq_empty_or_nonempty` `isPreconnected_empty` `Set.image_empty` `isConnected_iff` `IsConnected.isPreconnected` `IsPreconnected.image` `Continuous.continuousOn` `continuous_inl` `continuous_inr`

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_connectedComponent` 📖	mathematical	`Topology.IsQuotientMap` `IsConnected` `Set.preimage` `Set` `Set.instSingletonSet`	`Set.image` `connectedComponent`	—	`preimage_connectedComponent` `Set.image_preimage_eq` `surjective`
`preimage_connectedComponent` 📖	mathematical	`Topology.IsQuotientMap` `IsConnected` `Set.preimage` `Set` `Set.instSingletonSet`	`connectedComponent`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `IsConnected.subset_connectedComponent` `preimage_connectedComponent_connected` `isClosed_preimage` `mem_connectedComponent` `Continuous.mapsTo_connectedComponent` `continuous`

(root)

Definitions

Name	Category	Theorems
`connectedComponentSetoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`connectedComponent_subset_iInter_isClopen` 📖	mathematical	—	`Set` `Set.instHasSubset` `connectedComponent` `Set.iInter` `IsClopen` `Set.instMembership`	—	`Set.subset_iInter` `IsClopen.connectedComponent_subset`
`connectedComponents_preimage_image` 📖	mathematical	—	`Set.preimage` `ConnectedComponents` `Set.image` `Set.iUnion` `Set` `Set.instMembership` `connectedComponent`	—	`Set.image_eq_iUnion` `Set.preimage_iUnion₂` `Set.iUnion_congr_Prop` `connectedComponents_preimage_singleton`
`connectedComponents_preimage_singleton` 📖	mathematical	—	`Set.preimage` `ConnectedComponents` `Set` `Set.instSingletonSet` `connectedComponent`	—	`Set.ext` `Set.mem_preimage` `Set.mem_singleton_iff` `ConnectedComponents.coe_eq_coe'`
`connectedSpace_iff_clopen` 📖	mathematical	—	`ConnectedSpace` `Set` `Set.instEmptyCollection` `Set.univ`	—	`connectedSpace_iff_univ` `IsConnected.eq_1` `preconnectedSpace_iff_univ` `preconnectedSpace_iff_clopen` `Set.nonempty_iff_univ_nonempty`
`disjoint_or_subset_of_isClopen` 📖	mathematical	`IsPreconnected` `IsClopen`	`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`	—	`IsPreconnected.subset_isClopen` `Set.disjoint_or_nonempty_inter`
`frontier_eq_empty_iff` 📖	mathematical	—	`frontier` `Set` `Set.instEmptyCollection` `Set.univ`	—	`isClopen_iff_frontier_eq_empty` `isClopen_iff`
`instCompactSpaceConnectedComponents` 📖	mathematical	—	`CompactSpace` `ConnectedComponents` `ConnectedComponents.instTopologicalSpace`	—	`Quotient.compactSpace`
`isClopen_iff` 📖	mathematical	—	`IsClopen` `Set` `Set.instEmptyCollection` `Set.univ`	—	`by_contradiction` `nonempty_inter` `IsClosed.isOpen_compl` `Set.union_compl_self` `isClopen_empty` `isClopen_univ`
`isClopen_preimage_val` 📖	mathematical	`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` `frontier`	`IsClopen` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Set.preimage`	—	`isClosed_induced_iff` `isClosed_closure` `Set.image_val_injective` `Subtype.image_preimage_coe` `closure_eq_self_union_frontier` `Set.inter_union_distrib_left` `Set.inter_comm` `Disjoint.inter_eq` `Set.union_empty` `isOpen_induced`
`isConnected_iff_sUnion_disjoint_open` 📖	mathematical	—	`IsConnected` `Set` `Finset` `Finset.instMembership` `Set.instHasSubset`	—	`IsConnected.eq_1` `isPreconnected_iff_subset_of_disjoint` `Finset.induction_on` `Finset.coe_empty` `Set.sUnion_empty` `Set.Nonempty.not_subset_empty` `isOpen_sUnion` `Finset.coe_insert` `Set.sUnion_insert` `Set.subset_empty_iff` `instIsEmptyFalse` `Set.not_nonempty_iff_eq_empty` `Set.inter_self` `Set.inter_comm` `Finset.coe_singleton` `Set.sUnion_singleton`
`isPreconnected_iff_subset_of_disjoint` 📖	mathematical	—	`IsPreconnected` `Set` `Set.instHasSubset`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.not_nonempty_iff_eq_empty`
`isPreconnected_iff_subset_of_disjoint_closed` 📖	mathematical	—	`IsPreconnected` `Set` `Set.instHasSubset`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `isPreconnected_closed_iff` `Set.not_nonempty_iff_eq_empty`
`isPreconnected_iff_subset_of_fully_disjoint_closed` 📖	mathematical	—	`IsPreconnected` `Set` `Set.instHasSubset`	—	`isPreconnected_iff_subset_of_disjoint_closed` `Disjoint.inter_eq` `Set.inter_empty` `Set.subset_inter_iff` `IsClosed.inter` `Set.union_inter_distrib_right` `Set.subset_inter` `Set.Subset.rfl` `Set.disjoint_iff_inter_eq_empty` `Set.inter_inter_distrib_right` `Set.inter_comm`
`isPreconnected_of_forall_constant` 📖	mathematical	—	`IsPreconnected`	—	`Mathlib.Tactic.Push.not_forall_eq` `Set.eq_empty_iff_forall_notMem` `continuousOn_boolIndicator_iff_isClopen` `Set.preimage_subtype_coe_eq_compl` `IsOpen.isClosed_compl` `IsOpen.preimage` `continuous_subtype_val` `Set.mem_iff_boolIndicator` `Set.notMem_iff_boolIndicator`
`nonempty_frontier_iff` 📖	mathematical	—	`Set.Nonempty` `frontier`	—	—
`nonempty_inter` 📖	mathematical	`IsOpen` `Set` `Set.instUnion` `Set.univ` `Set.Nonempty`	`Set.instInter`	—	`Set.univ_inter` `PreconnectedSpace.isPreconnected_univ`
`preconnectedSpace_iff_clopen` 📖	mathematical	—	`PreconnectedSpace` `Set` `Set.instEmptyCollection` `Set.univ`	—	`isClopen_iff` `preconnectedSpace_of_forall_constant` `Set.preimage_compl` `Bool.compl_singleton` `IsClopen.preimage` `isClopen_discrete` `instDiscreteTopologyBool` `Set.compl_empty`
`preconnectedSpace_of_forall_constant` 📖	mathematical	—	`PreconnectedSpace`	—	`isPreconnected_of_forall_constant` `continuousOn_univ`
`preimage_connectedComponent_connected` 📖	mathematical	`IsConnected` `Set.preimage` `Set` `Set.instSingletonSet` `IsClosed`	`connectedComponent`	—	`Function.Surjective.of_comp` `Set.Nonempty.preimage` `connectedComponent_nonempty` `isClosed_connectedComponent` `isPreconnected_iff_subset_of_fully_disjoint_closed` `isPreconnected_iff_subset_of_disjoint_closed` `Set.Subset.trans` `Set.preimage_mono` `Set.singleton_subset_iff` `Disjoint.inter_eq` `Set.inter_empty` `Set.eq_of_subset_of_subset` `Set.biUnion_preimage_singleton` `Set.iUnion₂_subset` `Set.subset_inter` `Function.Surjective.preimage_subset_preimage_iff` `Set.mem_preimage` `Disjoint.subset_compl_right` `Disjoint.subset_compl_left` `IsClosed.inter` `Set.mem_union` `Disjoint.of_preimage` `Set.disjoint_iff_inter_eq_empty` `Set.inter_inter_distrib_left` `isPreconnected_connectedComponent` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Subset.antisymm_iff` `Set.inter_subset_right`
`subsingleton_of_disjoint_isClopen` 📖	—	`Set.Nonempty` `Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IsClopen`	—	—	`not_nontrivial_iff_subsingleton` `isClopen_iff` `Set.Nonempty.ne_empty` `Set.univ_inter`
`subsingleton_of_disjoint_isClosed_iUnion_eq_univ` 📖	—	`Set.Nonempty` `Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IsClosed` `Set.iUnion` `Set.univ`	—	—	`subsingleton_of_disjoint_isClopen` `isClosed_compl_iff` `Set.compl_eq_univ_diff` `Set.iUnion_diff` `isClosed_iUnion_of_finite` `eq_or_ne` `sdiff_self` `Disjoint.sdiff_eq_left`
`subsingleton_of_disjoint_isOpen_iUnion_eq_univ` 📖	—	`Set.Nonempty` `Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IsOpen` `Set.iUnion` `Set.univ`	—	—	`subsingleton_of_disjoint_isClopen` `isOpen_compl_iff` `Set.compl_eq_univ_diff` `Set.iUnion_diff` `isOpen_iUnion` `eq_or_ne` `sdiff_self` `Disjoint.sdiff_eq_left`

---

← Back to Index