Commit 2023-12-03 09:54 106c0998

View on Github →

feat(Topology/Order): continuity of Finset.sup, partialSups etc (#8141) Also rename Filter.Tendsto.sup_right_nhds to Filter.Tendsto.sup_nhds etc.

Estimated changes

added theorem partialSups_apply
added theorem Continuous.finset_inf'
added theorem Continuous.finset_inf
added theorem Continuous.finset_sup'
added theorem Continuous.finset_sup
added theorem Continuous.inf'
added theorem Continuous.sup'
added theorem ContinuousAt.inf'
added theorem ContinuousAt.inf
added theorem ContinuousAt.sup'
added theorem ContinuousAt.sup
added theorem ContinuousOn.inf'
added theorem ContinuousOn.inf
added theorem ContinuousOn.sup'
added theorem ContinuousOn.sup
added theorem ContinuousWithinAt.inf
added theorem ContinuousWithinAt.sup