CompactOpenCovered

📁 Source: Mathlib/Topology/Sets/CompactOpenCovered.lean

Statistics

Metric	Count
Definitions IsCompactOpenCovered	1
Theorems empty, exists_mem_of_isBasis, id_iff_isOpen_and_isCompact, iff_isCompactOpenCovered_sigmaMk, iff_of_unique, image, of_biUnion_eq_of_finite, of_biUnion_eq_of_isCompact, of_comp, of_finite, of_finite_of_isSpectralMap, of_iUnion_eq_of_finite, of_isCompact_of_forall_exists_isCompactOpenCovered, of_isOpenMap	14
Total	15

IsCompactOpenCovered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty 📖	mathematical	—	IsCompactOpenCovered Set Set.instEmptyCollection	—	Set.finite_empty isOpen_empty isCompact_empty Set.iUnion_congr_Prop Set.image_empty Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty
exists_mem_of_isBasis 📖	mathematical	TopologicalSpace.Opens.IsBasis IsCompact TopologicalSpace.Opens.carrier IsCompactOpenCovered	TopologicalSpace.Opens Set Set.instMembership Set.iUnion Set.image SetLike.coe TopologicalSpace.Opens.instSetLike	—	Finite.instSigma Set.ext Set.image_congr Set.iUnion_congr_Prop Set.mem_iUnion TopologicalSpace.Opens.coe_sSup TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact nonempty_fintype Function.Surjective.iUnion_comp Equiv.surjective
id_iff_isOpen_and_isCompact 📖	mathematical	—	IsCompactOpenCovered IsOpen IsCompact	—	iff_of_unique Set.image_congr Set.image_id' TopologicalSpace.Opens.is_open'
iff_isCompactOpenCovered_sigmaMk 📖	mathematical	—	IsCompactOpenCovered instTopologicalSpaceSigma	—	iff_of_unique isOpen_sigma_iff Set.mk_preimage_sigma TopologicalSpace.Opens.is_open' Set.mk_preimage_sigma_eq_empty Set.isCompact_sigma Set.ext IsCompact.sigma_exists_finite_sigma_eq Set.iUnion_congr_Prop Set.image_sigma_eq_iUnion Set.image_congr
iff_of_unique 📖	mathematical	—	IsCompactOpenCovered IsCompact Unique.instInhabited TopologicalSpace.Opens.carrier Set.image	—	Set.eq_empty_or_singleton_of_unique Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty Set.iUnion_iUnion_eq_left Set.finite_singleton
image 📖	mathematical	IsCompact SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	IsCompactOpenCovered Set.image	—	Set.finite_singleton Set.iUnion_congr_Prop Set.iUnion_iUnion_eq_left
of_biUnion_eq_of_finite 📖	—	Set.iUnion Set Set.instMembership IsCompactOpenCovered	—	—	Set.Finite.to_subtype of_iUnion_eq_of_finite Set.iUnion_coe_set Set.iUnion_congr_Prop
of_biUnion_eq_of_isCompact 📖	—	IsCompact Set.iUnion TopologicalSpace.Opens Set Set.instMembership SetLike.coe TopologicalSpace.Opens.instSetLike IsCompactOpenCovered	—	—	IsCompact.elim_finite_subcover TopologicalSpace.Opens.is_open' Set.iUnion_coe_set Set.iUnion_congr_Prop Set.instReflSubset of_biUnion_eq_of_finite subset_antisymm Set.instAntisymmSubset Finset.coe_image Set.iUnion_exists Set.biUnion_and' Set.iUnion_iUnion_eq_right subset_trans Set.instIsTransSubset Set.toFinite Finite.Set.finite_image Finite.of_fintype
of_comp 📖	—	PrespectralSpace Continuous IsOpen IsCompactOpenCovered	—	—	iff_isCompactOpenCovered_sigmaMk iff_of_unique Continuous.sigma_map PrespectralSpace.exists_isCompact_and_isOpen_between PrespectralSpace.sigma IsCompact.image IsOpen.preimage subset_antisymm Set.instAntisymmSubset Set.image_comp subset_trans Set.instIsTransSubset Set.image_mono Set.instReflSubset
of_finite 📖	mathematical	IsCompact TopologicalSpace.Opens.carrier Set.iUnion Set.image SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	IsCompactOpenCovered	—	of_iUnion_eq_of_finite image
of_finite_of_isSpectralMap 📖	mathematical	IsSpectralMap Set Set.instMembership Set.range IsOpen IsCompact	IsCompactOpenCovered	—	Set.finite_univ IsOpen.preimage IsSpectralMap.toContinuous IsCompact.preimage_of_isOpen subset_antisymm Set.instAntisymmSubset Set.iUnion_congr_Prop Set.iUnion_true Set.instReflSubset
of_iUnion_eq_of_finite 📖	—	Set.iUnion IsCompactOpenCovered	—	—	iff_isCompactOpenCovered_sigmaMk iff_of_unique TopologicalSpace.Opens.coe_iSup isCompact_iUnion Set.image_iUnion
of_isCompact_of_forall_exists_isCompactOpenCovered 📖	—	IsCompact Set Set.instHasSubset Set.instMembership IsOpen IsCompactOpenCovered	—	—	of_biUnion_eq_of_isCompact subset_antisymm Set.instAntisymmSubset Set.iUnion_exists
of_isOpenMap 📖	mathematical	PrespectralSpace Continuous IsOpenMap Set Set.instMembership Set.range IsOpen IsCompact	IsCompactOpenCovered	—	iff_isCompactOpenCovered_sigmaMk iff_of_unique IsOpenMap.exists_opens_image_eq_of_prespectralSpace PrespectralSpace.sigma continuous_sigma_iff isOpenMap_sigma

(root)

Definitions

Name	Category	Theorems
IsCompactOpenCovered 📖	MathDef	12 math math: IsCompactOpenCovered.of_finite_of_isSpectralMap, IsCompactOpenCovered.of_finite, IsCompactOpenCovered.image, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isCompact, IsCompactOpenCovered.of_isOpenMap, IsCompactOpenCovered.iff_isCompactOpenCovered_sigmaMk, IsCompactOpenCovered.iff_of_unique, AlgebraicGeometry.QuasiCompactCover.isCompactOpenCovered_of_isAffineOpen, AlgebraicGeometry.IsAffineOpen.isCompactOpenCovered, IsCompactOpenCovered.empty, AlgebraicGeometry.quasiCompactCover_iff, IsCompactOpenCovered.id_iff_isOpen_and_isCompact

---

← Back to Index