Commit 2023-02-21 07:40 9b9c4ecd

View on Github →

feat: Port Data.Analysis.Topology (#2399)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Analysis/Topology.lean

added def Compact.Realizer

added theorem Ctop.Realizer.ext'

added theorem Ctop.Realizer.ext

added theorem Ctop.Realizer.isClosed_iff

added theorem Ctop.Realizer.isOpen_iff

added theorem Ctop.Realizer.mem_interior_iff

added theorem Ctop.Realizer.nhds_F

added theorem Ctop.Realizer.nhds_σ

added def Ctop.Realizer.ofEquiv

added theorem Ctop.Realizer.ofEquiv_F

added theorem Ctop.Realizer.ofEquiv_σ

added theorem Ctop.Realizer.tendsto_nhds_iff

added structure Ctop.Realizer

added theorem Ctop.coe_mk

added theorem Ctop.mem_nhds_toTopsp

added def Ctop.ofEquiv

added theorem Ctop.ofEquiv_val

added def Ctop.toTopsp

added theorem Ctop.toTopsp_isTopologicalBasis

added structure Ctop

added theorem LocallyFinite.Realizer.to_locallyFinite

added structure LocallyFinite.Realizer

added theorem locallyFinite_iff_exists_realizer