ClopenBox

📁 Source: Mathlib/Topology/ClopenBox.lean

Statistics

Metric	Count
Definitions	0
Theorems countable_iff_secondCountable, countable_prod, exists_finset_eq_sup_prod, exists_prod_subset, finite_prod, surjective_finset_sup_prod	6
Total	6

TopologicalSpace.Clopens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_iff_secondCountable 📖	mathematical	—	Countable TopologicalSpace.Clopens SecondCountableTopology	—	Function.Injective.countable Function.Injective.of_eq_imp_le Eq.le TopologicalSpace.IsTopologicalBasis.eq_generateFrom loc_compact_Haus_tot_disc_of_zero_dim WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space instWeaklyLocallyCompactSpaceOfCompactSpace eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open TopologicalSpace.isBasis_countableBasis IsClosed.isCompact isClopen' ext Finset.countable Encodable.countable
countable_prod 📖	mathematical	—	Countable TopologicalSpace.Clopens instTopologicalSpaceProd	—	Function.Surjective.countable Finset.countable instCountableProd surjective_finset_sup_prod
exists_finset_eq_sup_prod 📖	mathematical	—	Finset.sup TopologicalSpace.Clopens instTopologicalSpaceProd Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra SProd.sprod instSProdProd	—	IsCompact.elim_nhds_subcover IsClosed.isCompact instCompactSpaceProd isClopen' IsOpen.mem_nhds IsClopen.isOpen Finset.sup_image le_antisymm Set.mem_iUnion₂ SetLike.le_def instIsConcreteLE Finset.le_sup Finset.sup_le Function.sometimes_spec exists_prod_subset
exists_prod_subset 📖	mathematical	TopologicalSpace.Clopens instTopologicalSpaceProd SetLike.instMembership instSetLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder SProd.sprod instSProdProd	—	Continuous.prodMk_right IsClosed.isCompact IsClosed.preimage isClopen' IsClopen.preimage ContinuousMap.isClopen_setOf_mapsTo ContinuousMap.continuous_toFun
finite_prod 📖	mathematical	—	Finite TopologicalSpace.Clopens instTopologicalSpaceProd	—	nonempty_fintype Finite.of_surjective Finite.of_fintype surjective_finset_sup_prod
surjective_finset_sup_prod 📖	mathematical	—	Finset TopologicalSpace.Clopens instTopologicalSpaceProd Finset.sup Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra SProd.sprod instSProdProd	—	exists_finset_eq_sup_prod

---

← Back to Index