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

Modified src/analysis/box_integral/partition/basic.lean

Modified src/analysis/convex/strict.lean

Modified src/topology/algebra/monoid.lean

Modified src/topology/algebra/order/field.lean

Modified src/topology/algebra/order/floor.lean

Created src/topology/algebra/order/group.lean

added theorem continuous_abs

added theorem tendsto_abs_nhds_within_zero

added theorem tendsto_zero_iff_abs_tendsto_zero

Modified src/topology/algebra/order/liminf_limsup.lean

Modified src/topology/algebra/order/monotone_continuity.lean

Modified src/topology/continuous_function/ordered.lean

Modified src/topology/order/basic.lean

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

deleted theorem tendsto_abs_nhds_within_zero

deleted theorem tendsto_zero_iff_abs_tendsto_zero

Modified src/topology/order/lower_topology.lean