Commit 2023-05-23 09:47 cd29f4ce

View on Github →

chore: forward-port leanprover-community/mathlib#18962 (#4209)

Estimated changes

Modified Mathlib/Order/Filter/CountableInter.lean

added inductive Filter.CountableGenerateSets

added def Filter.countableGenerate

added theorem Filter.countableGenerate_isGreatest

added theorem Filter.le_countableGenerate_iff_of_countableInterFilter

added theorem Filter.mem_countableGenerate_iff

Modified Mathlib/Topology/GDelta.lean

added theorem mem_residual_iff

added theorem residual_of_dense_Gδ

added theorem residual_of_dense_open

Modified Mathlib/Topology/MetricSpace/Baire.lean

modified theorem mem_residual