Clopen

📁 Source: Mathlib/Topology/Clopen.lean

Statistics

Metric	Count
Definitions	0
Theorems preimage_isClopen_of_isClopen, compl, diff, frontier_eq, himp, inter, isClosed, isOpen, preimage, prod, union, isClopen_biInter, isClopen_biUnion, isClopen_preimage, continuousOn_boolIndicator_iff_isClopen, continuous_boolIndicator_iff_isClopen, isClopen_biInter_finset, isClopen_biUnion_finset, isClopen_compl_iff, isClopen_discrete, isClopen_empty, isClopen_iInter_of_finite, isClopen_iUnion_of_finite, isClopen_iff_frontier_eq_empty, isClopen_inter_of_disjoint_cover_clopen, isClopen_of_disjoint_cover_open, isClopen_range_inl, isClopen_range_inr, isClopen_range_sigmaMk, isClopen_univ	30
Total	30

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_isClopen_of_isClopen 📖	mathematical	ContinuousOn IsClopen	Set Set.instInter Set.preimage	—	preimage_isClosed_of_isClosed isOpen_inter_preimage

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	IsClopen	Compl.compl Set Set.instCompl	—	IsOpen.isClosed_compl IsClosed.isOpen_compl
diff 📖	mathematical	IsClopen	Set Set.instSDiff	—	inter compl
frontier_eq 📖	mathematical	IsClopen	frontier Set Set.instEmptyCollection	—	isClopen_iff_frontier_eq_empty
himp 📖	mathematical	IsClopen	HImp.himp Set BooleanAlgebra.toHImp Set.instBooleanAlgebra	—	himp_eq union compl
inter 📖	mathematical	IsClopen	Set Set.instInter	—	IsClosed.inter IsOpen.inter
isClosed 📖	mathematical	IsClopen	IsClosed	—	—
isOpen 📖	mathematical	IsClopen	IsOpen	—	—
preimage 📖	mathematical	IsClopen Continuous	Set.preimage	—	IsClosed.preimage IsOpen.preimage
prod 📖	mathematical	IsClopen	instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	IsClosed.prod IsOpen.prod
union 📖	mathematical	IsClopen	Set Set.instUnion	—	IsClosed.union IsOpen.union

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClopen_biInter 📖	mathematical	IsClopen	Set.iInter Set Set.instMembership	—	isClosed_biInter isOpen_biInter
isClopen_biUnion 📖	mathematical	IsClopen	Set.iUnion Set Set.instMembership	—	isClosed_biUnion isOpen_biUnion

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClopen_preimage 📖	mathematical	Topology.IsQuotientMap	IsClopen Set.preimage	—	isClosed_preimage isOpen_preimage

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_boolIndicator_iff_isClopen 📖	mathematical	—	ContinuousOn instTopologicalSpaceBool Set.boolIndicator IsClopen Set Set.instMembership instTopologicalSpaceSubtype Set.preimage	—	continuousOn_iff_continuous_restrict continuous_boolIndicator_iff_isClopen
continuous_boolIndicator_iff_isClopen 📖	mathematical	—	Continuous instTopologicalSpaceBool Set.boolIndicator IsClopen	—	continuous_bool_rng Set.preimage_boolIndicator_true
isClopen_biInter_finset 📖	mathematical	IsClopen	Set.iInter Finset Finset.instMembership	—	Set.Finite.isClopen_biInter Finset.finite_toSet
isClopen_biUnion_finset 📖	mathematical	IsClopen	Set.iUnion Finset Finset.instMembership	—	Set.Finite.isClopen_biUnion Finset.finite_toSet
isClopen_compl_iff 📖	mathematical	—	IsClopen Compl.compl Set Set.instCompl	—	IsClopen.compl compl_compl
isClopen_discrete 📖	mathematical	—	IsClopen	—	isClosed_discrete isOpen_discrete
isClopen_empty 📖	mathematical	—	IsClopen Set Set.instEmptyCollection	—	isClosed_empty isOpen_empty
isClopen_iInter_of_finite 📖	mathematical	IsClopen	Set.iInter	—	isClosed_iInter isOpen_iInter_of_finite
isClopen_iUnion_of_finite 📖	mathematical	IsClopen	Set.iUnion	—	isClosed_iUnion_of_finite isOpen_iUnion
isClopen_iff_frontier_eq_empty 📖	mathematical	—	IsClopen frontier Set Set.instEmptyCollection	—	IsClopen.eq_1 closure_eq_iff_isClosed interior_eq_iff_isOpen frontier.eq_1 Set.diff_eq_empty Eq.subset Set.instReflSubset HasSubset.Subset.antisymm Set.instAntisymmSubset HasSubset.Subset.trans Set.instIsTransSubset interior_subset subset_closure
isClopen_inter_of_disjoint_cover_clopen 📖	mathematical	IsClopen Set Set.instHasSubset Set.instUnion IsOpen Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.instInter	—	IsClosed.inter isClosed_compl_iff HasSubset.Subset.antisymm Set.instAntisymmSubset Set.inter_subset_inter_right Disjoint.subset_compl_right Set.notMem_of_mem_compl IsOpen.inter
isClopen_of_disjoint_cover_open 📖	mathematical	Set Set.instHasSubset Set.univ Set.instUnion IsOpen 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	—	isClopen_inter_of_disjoint_cover_clopen isClopen_univ Set.univ_inter
isClopen_range_inl 📖	mathematical	—	IsClopen instTopologicalSpaceSum Set.range	—	isClosed_range_inl isOpen_range_inl
isClopen_range_inr 📖	mathematical	—	IsClopen instTopologicalSpaceSum Set.range	—	isClosed_range_inr isOpen_range_inr
isClopen_range_sigmaMk 📖	mathematical	—	IsClopen instTopologicalSpaceSigma Set.range	—	Topology.IsClosedEmbedding.isClosed_range Topology.IsClosedEmbedding.sigmaMk Topology.IsOpenEmbedding.isOpen_range Topology.IsOpenEmbedding.sigmaMk
isClopen_univ 📖	mathematical	—	IsClopen Set.univ	—	isClosed_univ isOpen_univ

---

← Back to Index