Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-03 03:01 84dc0bd6

View on Github →

chore(topology/order/basic): split (#18363) Move material that requires topological groups to a new file to reduce transitive imports.

Estimated changes

deleted theorem continuous.abs
deleted theorem continuous_abs
deleted theorem continuous_at.abs
deleted theorem continuous_on.abs
deleted theorem continuous_within_at.abs
deleted theorem filter.tendsto.abs