OpenCover

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

Statistics

Metric	Count
Definitions OpenCover, IsOpenCover	2
Theorems of_subset_iUnion, of_isOpenCover, comap, exists_mem, exists_mem_nhds, iSup_eq_top, iSup_set_eq_univ, iUnion_inter, isTopologicalBasis, mk, of_sets, isOpenCover, isOpenCover_mem_and_le	13
Total	15

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
OpenCover 📖	CompOp	—

IsPreirreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_subset_iUnion 📖	—	Pairwise Function.onFun TopologicalSpace.Opens Disjoint TopologicalSpace.Opens.instPartialOrder HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame IsPreirreducible SetLike.coe TopologicalSpace.Opens.instSetLike IsOpen Set Set.instHasSubset Set.iUnion	—	—	Set.eq_empty_or_nonempty isPreirreducible_empty exists_mem_irreducibleComponents_subset_of_isIrreducible open_subset IsClosed.isOpen_compl isClosed_of_mem_irreducibleComponents Set.not_subset Set.inter_nonempty_iff_exists_left Set.Nonempty.right TopologicalSpace.Opens.isOpen Set.not_disjoint_iff_nonempty_inter Set.mem_iUnion

PreirreducibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isOpenCover 📖	—	Pairwise Function.onFun TopologicalSpace.Opens Disjoint TopologicalSpace.Opens.instPartialOrder HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame TopologicalSpace.IsOpenCover PreirreducibleSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype	—	—	IsPreirreducible.of_subtype IsPreirreducible.of_subset_iUnion isOpen_univ TopologicalSpace.IsOpenCover.iSup_set_eq_univ

TopologicalSpace

Definitions

Name	Category	Theorems
IsOpenCover 📖	MathDef	5 math math: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, IsOpenCover.mk, Opens.IsBasis.isOpenCover, exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, IsOpenCover.of_sets

TopologicalSpace.IsOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	TopologicalSpace.IsOpenCover	DFunLike.coe FrameHom TopologicalSpace.Opens TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap	—	TopologicalSpace.Opens.is_open' isOpen_iUnion iSup_set_eq_univ
exists_mem 📖	mathematical	TopologicalSpace.IsOpenCover	TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike	—	iSup_set_eq_univ Set.mem_univ
exists_mem_nhds 📖	mathematical	TopologicalSpace.IsOpenCover	Set Filter Filter.instMembership nhds SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	exists_mem IsOpen.mem_nhds TopologicalSpace.Opens.isOpen
iSup_eq_top 📖	mathematical	TopologicalSpace.IsOpenCover	iSup TopologicalSpace.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
iSup_set_eq_univ 📖	mathematical	TopologicalSpace.IsOpenCover	Set.iUnion SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike Set.univ	—	TopologicalSpace.Opens.coe_iSup iSup_eq_top
iUnion_inter 📖	mathematical	TopologicalSpace.IsOpenCover	Set.iUnion Set Set.instInter SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	iSup_set_eq_univ Set.inter_univ
isTopologicalBasis 📖	mathematical	TopologicalSpace.IsOpenCover TopologicalSpace.IsTopologicalBasis TopologicalSpace.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike instTopologicalSpaceSubtype	Set.iUnion Set Set.image	—	TopologicalSpace.isTopologicalBasis_of_cover TopologicalSpace.Opens.is_open' iSup_set_eq_univ
mk 📖	mathematical	iSup TopologicalSpace.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	TopologicalSpace.IsOpenCover	—	—
of_sets 📖	mathematical	IsOpen Set.iUnion Set.univ	TopologicalSpace.IsOpenCover	—	isOpen_iUnion

TopologicalSpace.Opens.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenCover 📖	mathematical	TopologicalSpace.Opens.IsBasis	TopologicalSpace.IsOpenCover Set.Elem TopologicalSpace.Opens Set Set.instMembership	—	top_le_iff subset_trans Set.instIsTransSubset Eq.superset Set.instReflSubset TopologicalSpace.IsTopologicalBasis.sUnion_eq Set.sUnion_image isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_coe_set Set.iUnion_congr_Prop
isOpenCover_mem_and_le 📖	mathematical	TopologicalSpace.Opens.IsBasis TopologicalSpace.IsOpenCover	TopologicalSpace.Opens Set Set.instMembership Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	—	top_le_iff TopologicalSpace.IsOpenCover.exists_mem TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open TopologicalSpace.Opens.is_open' isOpen_iUnion

---

← Back to Index