Commit 2024-09-07 21:48 01c407bf

View on Github →

feat(Topology): lemas about MapClusterPt (#16572) Also reuse variables and make some arguments implicit.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/EverywherePos.lean

Modified Mathlib/Topology/Basic.lean

added theorem Filter.HasBasis.clusterPt_iff_frequently

added theorem Filter.HasBasis.mapClusterPt_iff_frequently

added theorem Filter.Tendsto.mapClusterPt

added theorem MapClusterPt.continuousAt_comp

added theorem MapClusterPt.mono

added theorem MapClusterPt.of_comp

added theorem MapClusterPt.tendsto_comp'

added theorem MapClusterPt.tendsto_comp

modified theorem mapClusterPt_comp

modified theorem mapClusterPt_def

modified theorem mapClusterPt_iff

modified theorem mapClusterPt_iff_ultrafilter

modified theorem mapClusterPt_of_comp

Modified Mathlib/Topology/Constructions.lean

added theorem MapClusterPt.curry_prodMap

added theorem MapClusterPt.prodMap

Modified Mathlib/Topology/UniformSpace/Cauchy.lean