Commit 2023-04-17 06:46 85576cf8

View on Github →

feat: port Topology.MetricSpace.Baire (#3315)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Baire.lean

added theorem Dense.inter_of_Gδ

added theorem IsGδ.dense_bunionᵢ_interior_of_closed

added theorem IsGδ.dense_unionᵢ_interior_of_closed

added theorem IsGδ.dense_unionₛ_interior_of_closed

added theorem dense_binterᵢ_of_Gδ

added theorem dense_binterᵢ_of_open

added theorem dense_bunionᵢ_interior_of_closed

added theorem dense_interᵢ_of_Gδ

added theorem dense_interᵢ_of_open

added theorem dense_interᵢ_of_open_nat

added theorem dense_interₛ_of_Gδ

added theorem dense_interₛ_of_open

added theorem dense_of_mem_residual

added theorem dense_unionᵢ_interior_of_closed

added theorem dense_unionₛ_interior_of_closed

added theorem eventually_residual

added theorem mem_residual

added theorem nonempty_interior_of_unionᵢ_of_closed