Commit 2023-07-08 15:27 adca8e20

View on Github →

feat: define HasCountableSeparatingOn (#5675)

Define a typeclass saying that a countable family of sets satisfying a given predicate separate points of a given set.
Provide instances for open and closed sets in a T₀ space with second countable topology and for measurable sets in case of a countably generated σ-algebra. See Zulip for motivation.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

Modified Mathlib/MeasureTheory/MeasurableSpaceDef.lean

added theorem MeasurableSpace.forall_generateFrom_mem_iff_mem_iff

Created Mathlib/Order/Filter/CountableSeparatingOn.lean

added theorem Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff

added theorem Filter.EventuallyEq.of_eventually_mem_of_forall_separating_preimage

added theorem Filter.EventuallyEq.of_forall_separating_mem_iff

added theorem Filter.EventuallyEq.of_forall_separating_preimage

added theorem Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating

added theorem Filter.exists_eventuallyEq_const_of_forall_separating

added theorem Filter.exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating

added theorem Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating

added theorem Filter.exists_singleton_mem_of_forall_separating

added theorem Filter.exists_singleton_mem_of_mem_of_forall_separating

added theorem Filter.exists_subset_subsingleton_mem_of_forall_separating

added theorem Filter.exists_subsingleton_mem_of_forall_separating

added theorem HasCountableSeparatingOn.mono

added theorem HasCountableSeparatingOn.of_subtype

added theorem exists_countable_separating

added theorem exists_nonempty_countable_separating

added theorem exists_seq_separating

Created Mathlib/Topology/CountableSeparatingOn.lean