Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-31 16:05 24e75f1e

View on Github →

chore(order/filter/basic): protect 3 lemmas (#18331)

Estimated changes

deleted theorem filter.tendsto.if'
deleted theorem filter.tendsto.if
deleted theorem filter.tendsto.piecewise