Commit 2023-01-31 07:39 17b73314

View on Github →

Fix: protect some lemmas (#1953) Backported in leanprover-community/mathlib#18331

Estimated changes

deleted theorem Filter.Tendsto.if'
deleted theorem Filter.Tendsto.if
deleted theorem Filter.Tendsto.piecewise