Commit 2024-10-08 08:32 3d1b50bd

View on Github →

feat(*): drop some TC assumptions about atTop (#17437) Whenever we're proving Tendsto _ atTop _, we can assume that the domain is nonempty and IsDirected α LE.le, because otherwise atTop is the trivial filter.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

modified theorem orthogonalProjection_tendsto_closure_iSup

modified theorem orthogonalProjection_tendsto_self

Modified Mathlib/Analysis/Normed/Field/Basic.lean

modified theorem NormedAddCommGroup.tendsto_atTop'

modified theorem NormedAddCommGroup.tendsto_atTop

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.tendsto_measure_Ici_atBot

modified theorem MeasureTheory.tendsto_measure_Ico_atTop

modified theorem MeasureTheory.tendsto_measure_Iic_atTop

modified theorem MeasureTheory.tendsto_measure_Ioc_atBot

modified theorem MeasureTheory.tendsto_measure_iInter

modified theorem MeasureTheory.tendsto_measure_iUnion_atBot

modified theorem MeasureTheory.tendsto_measure_iUnion_atTop

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.Tendsto.of_neBot_imp

Modified Mathlib/Topology/Basic.lean

modified theorem tendsto_atBot_of_eventually_const

modified theorem tendsto_atTop_of_eventually_const

Modified Mathlib/Topology/MetricSpace/ThickenedIndicator.lean