DisjointCover

📁 Source: Mathlib/Topology/Separation/DisjointCover.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, exists_finite_approximation_of_mem_nhds_diagonal, exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal, exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal, exists_finite_clopen_cover, exists_finite_nonempty_disjoint_clopen_cover, exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, exists_open_prod_subset_of_mem_nhds_diagonal	8
Total	8

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	Set.instMembership DFunLike.coe ContinuousMap instFunLike Set.instHasSubset Set.univ Set.iUnion SetLike.coe TopologicalSpace.Clopens TopologicalSpace.Clopens.instSetLike Pairwise Function.onFun Disjoint TopologicalSpace.Clopens.instPartialOrder HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra BooleanAlgebra.toBiheytingAlgebra TopologicalSpace.Clopens.instBooleanAlgebra	—	mem_nhdsSet_iff_forall ContinuousAt.preimage_mem_nhds Continuous.continuousAt ContinuousMapClass.map_continuous instContinuousMapClass
exists_finite_approximation_of_mem_nhds_diagonal 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	Continuous instTopologicalSpaceFin Set.instMembership DFunLike.coe ContinuousMap instFunLike	—	exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal Set.mem_iUnion Set.mem_univ Pairwise.eq continuous_discrete_rng instDiscreteTopologyFin Set.ext TopologicalSpace.Clopens.isOpen
exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	Set.instMembership DFunLike.coe ContinuousMap instFunLike Finset.sum Finset.univ Fin.fintype Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.coe TopologicalSpace.Clopens TopologicalSpace.Clopens.instSetLike	—	exists_finite_approximation_of_mem_nhds_diagonal IsClopen.preimage isClopen_discrete instDiscreteTopologyFin Fintype.sum_eq_single Set.indicator_of_notMem Set.indicator_of_mem
exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	Set.instMembership DFunLike.coe ContinuousMap instFunLike Finset.prod Finset.univ Fin.fintype Set.mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid SetLike.coe TopologicalSpace.Clopens TopologicalSpace.Clopens.instSetLike	—	exists_finite_approximation_of_mem_nhds_diagonal IsClopen.preimage isClopen_discrete instDiscreteTopologyFin Fintype.prod_eq_single Set.mulIndicator_of_notMem Set.mulIndicator_of_mem

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	IsOpenCover Finset SetLike.instMembership Finset.instSetLike Set.instHasSubset SProd.sprod Set.instSProd SetLike.coe Opens Opens.instSetLike	—	IsCompact.elim_finite_subcover isCompact_univ Set.mem_iUnion IsOpenCover.of_sets Set.iUnion_subtype Set.iUnion_congr_Prop exists_open_prod_subset_of_mem_nhds_diagonal
exists_open_prod_subset_of_mem_nhds_diagonal 📖	mathematical	Set Filter Filter.instMembership nhdsSet instTopologicalSpaceProd Set.diagonal	IsOpen Set.instMembership Set.instHasSubset SProd.sprod Set.instSProd	—	mem_nhdsSet_iff_forall mem_nhds_prod_iff' IsOpen.inter

TopologicalSpace.IsOpenCover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_clopen_cover 📖	mathematical	TopologicalSpace.IsOpenCover	Set Set.instHasSubset SetLike.coe TopologicalSpace.Clopens TopologicalSpace.Clopens.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike Set.univ Set.iUnion	—	IsCompact.elim_finite_subcover isCompact_univ Set.mem_iUnion Set.mem_iUnion₂ Set.mem_iUnion_of_mem Equiv.symm_apply_apply compact_exists_isClopen_in_isOpen TopologicalSpace.Opens.isOpen exists_mem
exists_finite_nonempty_disjoint_clopen_cover 📖	mathematical	TopologicalSpace.IsOpenCover	Set Set.instHasSubset SetLike.coe TopologicalSpace.Clopens TopologicalSpace.Clopens.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike Set.univ Set.iUnion Pairwise Function.onFun Disjoint TopologicalSpace.Clopens.instPartialOrder HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra BooleanAlgebra.toBiheytingAlgebra TopologicalSpace.Clopens.instBooleanAlgebra	—	exists_finite_clopen_cover Fintype.exists_disjointed_le Finset.mem_filter subset_trans Set.instIsTransSubset Set.mem_iUnion TopologicalSpace.Clopens.coe_finset_sup Set.iUnion_congr_Prop Set.iUnion_true Finset.mem_univ Equiv.symm_apply_apply Pairwise.comp_of_injective Subtype.val_injective Equiv.injective

---

← Back to Index