Commit 2023-02-01 00:30 3e45c8eb

View on Github →

feat: port Topology.Bases (#1910)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Bases.lean

added theorem Dense.exists_countable_dense_subset

added theorem Dense.exists_countable_dense_subset_bot_top

added theorem QuotientMap.secondCountableTopology

added theorem Set.Countable.isSeparable

added theorem Set.Finite.isSeparable

added theorem Set.PairwiseDisjoint.countable_of_isOpen

added theorem Set.PairwiseDisjoint.countable_of_nonempty_interior

added theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq

added theorem TopologicalSpace.IsSeparable.closure

added theorem TopologicalSpace.IsSeparable.image

added theorem TopologicalSpace.IsSeparable.mono

added theorem TopologicalSpace.IsSeparable.union

added def TopologicalSpace.IsSeparable

added theorem TopologicalSpace.IsTopologicalBasis.dense_iff

added theorem TopologicalSpace.IsTopologicalBasis.diff_empty

added theorem TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset

added theorem TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open

added theorem TopologicalSpace.IsTopologicalBasis.insert_empty

added theorem TopologicalSpace.IsTopologicalBasis.isOpenMap_iff

added theorem TopologicalSpace.IsTopologicalBasis.isOpen_iff

added theorem TopologicalSpace.IsTopologicalBasis.mem_closure_iff

added theorem TopologicalSpace.IsTopologicalBasis.mem_nhds_iff

added theorem TopologicalSpace.IsTopologicalBasis.nhds_hasBasis

added theorem TopologicalSpace.IsTopologicalBasis.open_eq_unionᵢ

added theorem TopologicalSpace.IsTopologicalBasis.open_eq_unionₛ'

added theorem TopologicalSpace.IsTopologicalBasis.open_eq_unionₛ

added theorem TopologicalSpace.IsTopologicalBasis.open_iff_eq_unionₛ

added theorem TopologicalSpace.IsTopologicalBasis.quotient

added theorem TopologicalSpace.IsTopologicalBasis.quotientMap

added theorem TopologicalSpace.IsTopologicalBasis.sigma

added theorem TopologicalSpace.IsTopologicalBasis.sum

added structure TopologicalSpace.IsTopologicalBasis

added theorem TopologicalSpace.Quotient.secondCountableTopology

added theorem TopologicalSpace.SecondCountableTopology.mk'

added def TopologicalSpace.countableBasis

added theorem TopologicalSpace.countable_countableBasis

added theorem TopologicalSpace.countable_cover_nhds

added theorem TopologicalSpace.countable_cover_nhdsWithin

added theorem TopologicalSpace.denseRange_denseSeq

added def TopologicalSpace.denseSeq

added theorem TopologicalSpace.empty_nmem_countableBasis

added theorem TopologicalSpace.eq_generateFrom_countableBasis

added theorem TopologicalSpace.exists_countable_basis

added theorem TopologicalSpace.exists_countable_dense

added theorem TopologicalSpace.exists_dense_seq

added theorem TopologicalSpace.isBasis_countableBasis

added theorem TopologicalSpace.isOpen_of_mem_countableBasis

added theorem TopologicalSpace.isOpen_unionᵢ_countable

added theorem TopologicalSpace.isOpen_unionₛ_countable

added theorem TopologicalSpace.isSeparable_of_separableSpace

added theorem TopologicalSpace.isSeparable_of_separableSpace_subtype

added theorem TopologicalSpace.isSeparable_unionᵢ

added theorem TopologicalSpace.isSeparable_univ_iff

added theorem TopologicalSpace.isTopologicalBasis_of_cover

added theorem TopologicalSpace.isTopologicalBasis_of_open_of_nhds

added theorem TopologicalSpace.isTopologicalBasis_of_subbasis

added theorem TopologicalSpace.isTopologicalBasis_opens

added theorem TopologicalSpace.nonempty_of_mem_countableBasis

added theorem TopologicalSpace.secondCountableTopology_induced

added theorem TopologicalSpace.secondCountableTopology_infᵢ

added theorem TopologicalSpace.secondCountableTopology_of_countable_cover

added theorem TopologicalSpace.separableSpace_of_denseRange

added theorem exists_countable_dense_bot_top

added theorem isTopologicalBasis_infᵢ

added theorem isTopologicalBasis_pi

added theorem isTopologicalBasis_singletons