Constructible

📁 Source: Mathlib/Topology/Constructible.lean

Statistics

Metric	Count
Definitions IsRetrocompact, IsConstructible, IsLocallyConstructible	3
Theorems isConstructible, isRetrocompact, biInter, biUnion, empty, finsetInf, finsetInf', finsetSup, finsetSup', iInter, iUnion, image_of_isEmbedding, inter, inter_isOpen, isCompact, isConstructible, isLocallyConstructible, isOpen_inter, preimage_of_isClosedEmbedding, preimage_of_isOpenEmbedding, sInter, sUnion, singleton, union, univ, IsRetrocompact_iff_isSpectralMap_subtypeVal, isRetrocompact_iff_isCompact, of_isOpenCover, biInter, biUnion, compl, empty, empty_union_induction, himp, iInter, iUnion, image_of_isClosedEmbedding, image_of_isOpenEmbedding, induction_of_isTopologicalBasis, inter, isLocallyConstructible, of_compl, preimage, preimage_of_isClosedEmbedding, preimage_of_isOpenEmbedding, sInter, sUnion, sdiff, union, univ, biUnion, empty, finsetInf, finsetInf', iInter, iUnion, iff_isConstructible_of_isOpenCover, iff_of_isOpenCover, inter, inter_of_isOpen_isCompact, isConstructible, isConstructible_of_subset_of_isCompact, of_isOpenCover, of_isOpenCover', preimage_of_isOpenEmbedding, sInter, sUnion, union, univ, isConstructible_compl, isConstructible_preimage_iff_of_isOpenEmbedding	71
Total	74

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConstructible 📖	mathematical	IsCompact IsOpen	Topology.IsConstructible	—	IsRetrocompact.isConstructible isRetrocompact
isRetrocompact 📖	mathematical	IsCompact IsOpen	IsRetrocompact	—	inter_of_isOpen

IsRetrocompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter 📖	mathematical	IsRetrocompact	Set.iInter Set Set.instMembership	—	InfClosed.biInf_mem univ
biUnion 📖	mathematical	IsRetrocompact	Set.iUnion Set Set.instMembership	—	SupClosed.biSup_mem empty
empty 📖	mathematical	—	IsRetrocompact Set Set.instEmptyCollection	—	Set.empty_inter
finsetInf 📖	mathematical	IsRetrocompact	Finset.inf Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	Finset.cons_induction Finset.inf_cons inter Finset.forall_of_forall_cons
finsetInf' 📖	mathematical	Finset.Nonempty IsRetrocompact	Finset.inf' Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Finset.inf'_eq_inf finsetInf
finsetSup 📖	mathematical	IsRetrocompact	Finset.sup Set Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Finset.cons_induction Finset.sup_empty Finset.sup_cons union Finset.forall_of_forall_cons
finsetSup' 📖	mathematical	Finset.Nonempty IsRetrocompact	Finset.sup' Set Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Finset.sup'_eq_sup finsetSup
iInter 📖	mathematical	IsRetrocompact	Set.iInter	—	InfClosed.iInf_mem univ
iUnion 📖	mathematical	IsRetrocompact	Set.iUnion	—	SupClosed.iSup_mem empty
image_of_isEmbedding 📖	mathematical	IsRetrocompact Topology.IsEmbedding Set.range	Set.image	—	Set.image_inter_preimage Topology.IsEmbedding.isCompact_iff Set.image_preimage_eq_inter_range Set.inter_comm IsOpen.preimage Topology.IsEmbedding.continuous
inter 📖	mathematical	IsRetrocompact	Set Set.instInter	—	IsCompact.inter Set.inter_inter_distrib_right
inter_isOpen 📖	mathematical	IsRetrocompact IsOpen	Set Set.instInter	—	IsOpen.inter Set.inter_assoc
isCompact 📖	mathematical	IsRetrocompact	IsCompact	—	Set.inter_univ CompactSpace.isCompact_univ
isConstructible 📖	mathematical	IsOpen IsRetrocompact	Topology.IsConstructible	—	BooleanSubalgebra.subset_closure
isLocallyConstructible 📖	mathematical	IsOpen IsRetrocompact	Topology.IsLocallyConstructible	—	Topology.IsConstructible.isLocallyConstructible isConstructible
isOpen_inter 📖	mathematical	IsRetrocompact IsOpen	Set Set.instInter	—	inter_isOpen Set.inter_comm
preimage_of_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding IsCompact Compl.compl Set Set.instCompl Set.range IsRetrocompact	Set.preimage	—	Set.range_diff_image Topology.IsEmbedding.injective Topology.IsClosedEmbedding.toIsEmbedding sdiff_eq Set.compl_inter compl_compl Set.union_comm IsClosed.isOpen_compl Topology.IsClosedEmbedding.isClosedMap IsOpen.isClosed_compl IsCompact.union IsCompact.image Topology.IsClosedEmbedding.continuous Topology.IsEmbedding.isCompact_iff Set.image_preimage_inter Set.inter_union_distrib_left Set.inter_left_comm Set.inter_eq_right Set.image_subset_range Set.inter_compl_self Set.inter_empty Set.union_empty IsCompact.inter_left Topology.IsClosedEmbedding.isClosed_range
preimage_of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding IsRetrocompact	Set.preimage	—	Topology.IsEmbedding.isCompact_iff Topology.IsOpenEmbedding.toIsEmbedding Set.image_preimage_inter IsCompact.image Topology.IsOpenEmbedding.continuous Topology.IsOpenEmbedding.isOpenMap
sInter 📖	mathematical	IsRetrocompact	Set.sInter	—	InfClosed.sInf_mem univ
sUnion 📖	mathematical	IsRetrocompact	Set.sUnion	—	SupClosed.sSup_mem empty
singleton 📖	mathematical	—	IsRetrocompact Set Set.instSingletonSet	—	Set.Subsingleton.isCompact Set.Subsingleton.singleton_inter
union 📖	mathematical	IsRetrocompact	Set Set.instUnion	—	IsCompact.union Set.union_inter_distrib_right
univ 📖	mathematical	—	IsRetrocompact Set.univ	—	Set.univ_inter

QuasiSeparatedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRetrocompact_iff_isCompact 📖	mathematical	IsOpen	IsRetrocompact IsCompact	—	IsRetrocompact.isCompact IsCompact.isRetrocompact
of_isOpenCover 📖	mathematical	TopologicalSpace.IsOpenCover IsRetrocompact SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike IsQuasiSeparated	QuasiSeparatedSpace	—	IsCompact.elim_finite_subcover TopologicalSpace.Opens.is_open' TopologicalSpace.IsOpenCover.iSup_set_eq_univ subset_antisymm Set.instAntisymmSubset Set.mem_iUnion₂ Finset.isCompact_biUnion Set.inter_subset_left IsOpen.inter

Topology

Definitions

Name	Category	Theorems
IsConstructible 📖	MathDef	14 math math: IsConstructible.empty, IsCompact.isConstructible, IsLocallyConstructible.iff_isConstructible_of_isOpenCover, PrimeSpectrum.isConstructible_basicOpen, IsLocallyConstructible.isConstructible, IsLocallyConstructible.inter_of_isOpen_isCompact, isConstructible_compl, PrimeSpectrum.ConstructibleSetData.isConstructible_toSet, PrimeSpectrum.exists_constructibleSetData_iff, IsLocallyConstructible.isConstructible_of_subset_of_isCompact, IsConstructible.univ, isConstructible_preimage_iff_of_isOpenEmbedding, IsRetrocompact.isConstructible, PrimeSpectrum.isConstructible_range_comap
IsLocallyConstructible 📖	MathDef	6 math math: IsConstructible.isLocallyConstructible, IsLocallyConstructible.iff_of_isOpenCover, IsLocallyConstructible.iff_isConstructible_of_isOpenCover, IsLocallyConstructible.univ, IsLocallyConstructible.empty, IsRetrocompact.isLocallyConstructible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConstructible_compl 📖	mathematical	—	IsConstructible Compl.compl Set Set.instCompl	—	BooleanSubalgebra.compl_mem_iff
isConstructible_preimage_iff_of_isOpenEmbedding 📖	mathematical	IsOpenEmbedding IsRetrocompact Set.range Set Set.instHasSubset	IsConstructible Set.preimage	—	Set.image_preimage_eq_range_inter Set.inter_eq_right IsConstructible.image_of_isOpenEmbedding IsConstructible.preimage_of_isOpenEmbedding

Topology.IsConstructible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter 📖	mathematical	Topology.IsConstructible	Set.iInter Set Set.instMembership	—	BooleanSubalgebra.biInf_mem
biUnion 📖	mathematical	Topology.IsConstructible	Set.iUnion Set Set.instMembership	—	BooleanSubalgebra.biSup_mem
compl 📖	mathematical	Topology.IsConstructible	Compl.compl Set Set.instCompl	—	Topology.isConstructible_compl
empty 📖	mathematical	—	Topology.IsConstructible Set Set.instEmptyCollection	—	BooleanSubalgebra.bot_mem
empty_union_induction 📖	—	BooleanSubalgebra.subset_closure Set Set.instBooleanAlgebra setOf IsOpen IsRetrocompact Set.instUnion union Compl.compl Set.instCompl compl Topology.IsConstructible	—	—	BooleanSubalgebra.subset_closure union compl BooleanSubalgebra.closure_bot_sup_induction isOpen_empty IsRetrocompact.empty
himp 📖	mathematical	Topology.IsConstructible	HImp.himp Set BooleanAlgebra.toHImp Set.instBooleanAlgebra	—	BooleanSubalgebra.himp_mem
iInter 📖	mathematical	Topology.IsConstructible	Set.iInter	—	BooleanSubalgebra.iInf_mem
iUnion 📖	mathematical	Topology.IsConstructible	Set.iUnion	—	BooleanSubalgebra.iSup_mem
image_of_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding IsRetrocompact Compl.compl Set Set.instCompl Set.range Topology.IsConstructible	Set.image	—	empty_union_induction Set.range_diff_image Topology.IsEmbedding.injective Topology.IsClosedEmbedding.toIsEmbedding sdiff_eq Set.compl_inter compl_compl Set.union_comm IsClosed.isOpen_compl Topology.IsClosedEmbedding.isClosedMap IsOpen.isClosed_compl Set.union_inter_distrib_right Set.image_inter_preimage IsCompact.union IsCompact.image Topology.IsClosedEmbedding.isCompact_preimage IsOpen.preimage Topology.IsClosedEmbedding.continuous sdiff_compl Set.inter_eq_left Set.image_subset_range Set.compl_inter_self Set.union_empty sdiff IsRetrocompact.isConstructible Topology.IsClosedEmbedding.isClosed_range Set.image_union union of_compl
image_of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding IsRetrocompact Set.range Topology.IsConstructible	Set.image	—	empty_union_induction IsRetrocompact.isConstructible Topology.IsOpenEmbedding.isOpenMap IsRetrocompact.image_of_isEmbedding Topology.IsOpenEmbedding.isEmbedding Set.image_union union Set.range_diff_image Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding sdiff Topology.IsOpenEmbedding.isOpen_range
induction_of_isTopologicalBasis 📖	—	TopologicalSpace.IsTopologicalBasis Set.range Set IsCompact Set.instSDiff Set.iUnion Set.instMembership sdiff IsCompact.isConstructible TopologicalSpace.IsTopologicalBasis.isOpen biUnion Set.instUnion union Topology.IsConstructible	—	—	sdiff IsCompact.isConstructible TopologicalSpace.IsTopologicalBasis.isOpen biUnion union BooleanSubalgebra.closure_sdiff_sup_induction IsOpen.union IsRetrocompact.union IsOpen.inter IsRetrocompact.inter_isOpen isOpen_empty IsRetrocompact.empty isOpen_univ IsRetrocompact.univ isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis BooleanSubalgebra.sdiff_mem BooleanSubalgebra.subset_closure IsRetrocompact.isCompact Set.iUnion_diff Set.Finite.induction_on Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.iUnion_iUnion_eq_left sdiff_self Set.biUnion_insert isOpen_biUnion IsRetrocompact.biUnion IsCompact.isRetrocompact
inter 📖	mathematical	Topology.IsConstructible	Set Set.instInter	—	BooleanSubalgebra.inf_mem
isLocallyConstructible 📖	mathematical	Topology.IsConstructible	Topology.IsLocallyConstructible	—	Topology.isConstructible_preimage_iff_of_isOpenEmbedding IsOpen.isOpenEmbedding_subtypeVal isOpen_univ Subtype.range_coe_subtype
of_compl 📖	—	Topology.IsConstructible Compl.compl Set Set.instCompl	—	—	Topology.isConstructible_compl
preimage 📖	—	Continuous IsRetrocompact Set.preimage Topology.IsConstructible	—	—	empty_union_induction IsRetrocompact.isConstructible IsOpen.preimage Set.preimage_union union Set.preimage_compl compl
preimage_of_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding IsCompact Compl.compl Set Set.instCompl Set.range Topology.IsConstructible	Set.preimage	—	preimage Topology.IsClosedEmbedding.continuous IsRetrocompact.preimage_of_isClosedEmbedding
preimage_of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding Topology.IsConstructible	Set.preimage	—	preimage Topology.IsOpenEmbedding.continuous IsRetrocompact.preimage_of_isOpenEmbedding
sInter 📖	mathematical	Topology.IsConstructible	Set.sInter	—	BooleanSubalgebra.sInf_mem
sUnion 📖	mathematical	Topology.IsConstructible	Set.sUnion	—	BooleanSubalgebra.sSup_mem
sdiff 📖	mathematical	Topology.IsConstructible	Set Set.instSDiff	—	BooleanSubalgebra.sdiff_mem
union 📖	mathematical	Topology.IsConstructible	Set Set.instUnion	—	BooleanSubalgebra.sup_mem
univ 📖	mathematical	—	Topology.IsConstructible Set.univ	—	BooleanSubalgebra.top_mem

Topology.IsLocallyConstructible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biUnion 📖	mathematical	Topology.IsLocallyConstructible	Set.iUnion Set Set.instMembership	—	SupClosed.biSup_mem union empty
empty 📖	mathematical	—	Topology.IsLocallyConstructible Set Set.instEmptyCollection	—	Topology.IsConstructible.isLocallyConstructible Topology.IsConstructible.empty
finsetInf 📖	mathematical	Topology.IsLocallyConstructible	Finset.inf Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	Finset.cons_induction Finset.inf_cons inter Finset.forall_of_forall_cons
finsetInf' 📖	mathematical	Finset.Nonempty Topology.IsLocallyConstructible	Finset.inf' Set Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Finset.inf'_eq_inf finsetInf
iInter 📖	mathematical	Topology.IsLocallyConstructible	Set.iInter	—	InfClosed.iInf_mem univ
iUnion 📖	mathematical	Topology.IsLocallyConstructible	Set.iUnion	—	SupClosed.iSup_mem union empty
iff_isConstructible_of_isOpenCover 📖	mathematical	TopologicalSpace.IsOpenCover IsCompact SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	Topology.IsLocallyConstructible Topology.IsConstructible Set Set.instInter	—	inter_of_isOpen_isCompact TopologicalSpace.Opens.is_open' of_isOpenCover' Topology.IsConstructible.isLocallyConstructible
iff_of_isOpenCover 📖	mathematical	TopologicalSpace.IsOpenCover	Topology.IsLocallyConstructible Set.Elem SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	preimage_of_isOpenEmbedding IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open' of_isOpenCover
inter 📖	mathematical	Topology.IsLocallyConstructible	Set Set.instInter	—	Filter.inter_mem IsOpen.inter Topology.IsConstructible.inter Set.inter_subset_left Set.inter_subset_right Topology.IsConstructible.preimage_of_isOpenEmbedding Topology.IsOpenEmbedding.inclusion IsOpen.preimage continuous_subtype_val
inter_of_isOpen_isCompact 📖	mathematical	Topology.IsLocallyConstructible IsOpen IsCompact	Topology.IsConstructible Set Set.instInter	—	isConstructible_of_subset_of_isCompact inter Topology.IsConstructible.isLocallyConstructible IsCompact.isConstructible Set.inter_subset_right
isConstructible 📖	mathematical	Topology.IsLocallyConstructible	Topology.IsConstructible	—	isConstructible_of_subset_of_isCompact Set.subset_univ isCompact_univ
isConstructible_of_subset_of_isCompact 📖	mathematical	Topology.IsLocallyConstructible Set Set.instHasSubset IsCompact	Topology.IsConstructible	—	TopologicalSpace.IsTopologicalBasis.mem_nhds_iff PrespectralSpace.isTopologicalBasis Topology.IsConstructible.preimage_of_isOpenEmbedding Topology.IsOpenEmbedding.restrict Topology.IsOpenEmbedding.id Topology.IsConstructible.image_of_isOpenEmbedding IsOpen.isOpenEmbedding_subtypeVal Subtype.range_coe_subtype IsCompact.isRetrocompact Subtype.image_preimage_coe IsCompact.elim_nhds_subcover IsOpen.mem_nhds subset_antisymm Set.instAntisymmSubset Set.iUnion₂_inter Set.subset_inter_iff HasSubset.Subset.trans Set.instIsTransSubset subset_rfl Set.instReflSubset Set.iUnion₂_subset Set.inter_subset_right Topology.IsConstructible.biUnion Finset.finite_toSet
of_isOpenCover 📖	—	TopologicalSpace.IsOpenCover Topology.IsLocallyConstructible Set.Elem SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	—	TopologicalSpace.IsOpenCover.exists_mem Topology.IsOpenEmbedding.image_mem_nhds IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open' IsOpen.isOpenMap_subtype_val Subtype.val_injective Topology.IsOpenEmbedding.isInducing Topology.IsOpenEmbedding.restrict Set.image_congr Set.ext Function.Injective.mem_set_image Equiv.Set.image_symm_apply Topology.IsConstructible.preimage_of_isOpenEmbedding Homeomorph.isOpenEmbedding
of_isOpenCover' 📖	—	TopologicalSpace.IsOpenCover Topology.IsLocallyConstructible Set Set.instInter SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	—	of_isOpenCover Subtype.preimage_coe_inter_self preimage_of_isOpenEmbedding IsOpen.isOpenEmbedding_subtypeVal TopologicalSpace.Opens.is_open'
preimage_of_isOpenEmbedding 📖	mathematical	Topology.IsLocallyConstructible Topology.IsOpenEmbedding	Set.preimage	—	ContinuousAt.preimage_mem_nhds Continuous.continuousAt Topology.IsOpenEmbedding.continuous IsOpen.preimage Topology.IsConstructible.preimage_of_isOpenEmbedding Topology.IsOpenEmbedding.restrictPreimage
sInter 📖	mathematical	Topology.IsLocallyConstructible	Set.sInter	—	InfClosed.sInf_mem univ
sUnion 📖	mathematical	Topology.IsLocallyConstructible	Set.sUnion	—	SupClosed.sSup_mem union empty
union 📖	mathematical	Topology.IsLocallyConstructible	Set Set.instUnion	—	Filter.inter_mem IsOpen.inter Set.inter_subset_left Set.inter_subset_right Set.ext Topology.IsConstructible.union Topology.IsConstructible.preimage_of_isOpenEmbedding Topology.IsOpenEmbedding.inclusion IsOpen.preimage continuous_subtype_val
univ 📖	mathematical	—	Topology.IsLocallyConstructible Set.univ	—	Topology.IsConstructible.isLocallyConstructible Topology.IsConstructible.univ

(root)

Definitions

Name	Category	Theorems
IsRetrocompact 📖	MathDef	10 math math: PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg, IsRetrocompact_iff_isSpectralMap_subtypeVal, IsRetrocompact.singleton, IsRetrocompact.empty, IsCompact.isRetrocompact, AlgebraicGeometry.isRetrocompact_basicOpen, PrimeSpectrum.isRetrocompact_zeroLocus_compl, QuasiSeparatedSpace.isRetrocompact_iff_isCompact, PrimeSpectrum.isRetrocompact_basicOpen, IsRetrocompact.univ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsRetrocompact_iff_isSpectralMap_subtypeVal 📖	mathematical	—	IsRetrocompact IsSpectralMap Set Set.instMembership instTopologicalSpaceSubtype	—	continuous_subtype_val Topology.IsEmbedding.isCompact_iff Topology.IsEmbedding.subtypeVal Set.image_preimage_eq_inter_range Subtype.range_coe_subtype Set.setOf_mem_eq Set.inter_comm Subtype.image_preimage_coe IsCompact.image IsSpectralMap.isCompact_preimage_of_isOpen

---

← Back to Index