Commit 2023-02-06 07:35 b867de33

View on Github →

feat: port Topology.GDelta (#2064)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/GDelta.lean

added theorem Finset.isGδ_compl

added theorem IsClosed.isGδ

added theorem IsGδ.inter

added theorem IsGδ.union

added def IsGδ

added theorem IsOpen.isGδ

added theorem Set.Countable.isGδ_compl

added theorem Set.Finite.isGδ

added theorem Set.Finite.isGδ_compl

added theorem Set.Subsingleton.isGδ_compl

added theorem isGδ_binterᵢ

added theorem isGδ_binterᵢ_of_open

added theorem isGδ_bunionᵢ

added theorem isGδ_compl_singleton

added theorem isGδ_empty

added theorem isGδ_interᵢ

added theorem isGδ_interᵢ_of_open

added theorem isGδ_interₛ

added theorem isGδ_setOf_continuousAt

added theorem isGδ_singleton

added theorem isGδ_univ

added def residual