Commit 2023-08-09 17:44 6cb2b8d5

View on Github →

feat: Summable.countable_support (#6473) A step towards showing that Pmfs have countable support. Thanks Eric Rodriguez and Kevin Buzzard for helping on zulip.

Estimated changes

Modified Mathlib/Order/Filter/Cofinite.lean

added theorem Filter.Tendsto.countable_compl_preimage_sInter_sets

added theorem Filter.countable_compl_sInter_sets

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem Summable.countable_support

Modified Mathlib/Topology/Inseparable.lean

added theorem sInter_nhds_sets_eq_specializes

Modified Mathlib/Topology/Instances/ENNReal.lean

added theorem Summable.countable_support_ennreal

added theorem Summable.countable_support_nnreal

Modified Mathlib/Topology/Separation.lean

added theorem sInter_sets_nhds