Commit 2021-05-14 14:25 f8dc7224

View on Github →

refactor(topology/algebra/ordered): reduce imports (#7601) Renames topology.algebra.ordered to topology.algebra.order, and moves the material about liminf/limsup and about extend_from to separate files, in order to delay imports.

Estimated changes

Modified src/algebra/continued_fractions/computation/approximation_corollaries.lean

Modified src/analysis/calculus/local_extr.lean

Modified src/analysis/normed_space/basic.lean

Modified src/topology/algebra/floor_ring.lean

Renamed src/topology/algebra/ordered.lean to src/topology/algebra/ordered/basic.lean

deleted theorem Liminf_eq_of_le_nhds

deleted theorem Liminf_nhds

deleted theorem Limsup_eq_of_le_nhds

deleted theorem Limsup_nhds

deleted theorem continuous_on_Icc_extend_from_Ioo

deleted theorem continuous_on_Ico_extend_from_Ioo

deleted theorem continuous_on_Ioc_extend_from_Ioo

deleted theorem eq_lim_at_left_extend_from_Ioo

deleted theorem eq_lim_at_right_extend_from_Ioo

deleted theorem filter.tendsto.is_bounded_under_ge

deleted theorem filter.tendsto.is_bounded_under_le

deleted theorem filter.tendsto.is_cobounded_under_ge

deleted theorem filter.tendsto.is_cobounded_under_le

deleted theorem filter.tendsto.liminf_eq

deleted theorem filter.tendsto.limsup_eq

deleted theorem gt_mem_sets_of_Liminf_gt

deleted theorem is_bounded_ge_nhds

deleted theorem is_bounded_le_nhds

deleted theorem is_cobounded_ge_nhds

deleted theorem is_cobounded_le_nhds

deleted theorem le_nhds_of_Limsup_eq_Liminf

deleted theorem lt_mem_sets_of_Limsup_lt

deleted theorem tendsto_of_le_liminf_of_limsup_le

deleted theorem tendsto_of_liminf_eq_limsup

Created src/topology/algebra/ordered/extend_from.lean

added theorem continuous_on_Icc_extend_from_Ioo

added theorem continuous_on_Ico_extend_from_Ioo

added theorem continuous_on_Ioc_extend_from_Ioo

added theorem eq_lim_at_left_extend_from_Ioo

added theorem eq_lim_at_right_extend_from_Ioo

Created src/topology/algebra/ordered/liminf_limsup.lean

added theorem Liminf_eq_of_le_nhds

added theorem Liminf_nhds

added theorem Limsup_eq_of_le_nhds

added theorem Limsup_nhds

added theorem filter.tendsto.is_bounded_under_ge

added theorem filter.tendsto.is_bounded_under_le

added theorem filter.tendsto.is_cobounded_under_ge

added theorem filter.tendsto.is_cobounded_under_le

added theorem filter.tendsto.liminf_eq

added theorem filter.tendsto.limsup_eq

added theorem gt_mem_sets_of_Liminf_gt

added theorem is_bounded_ge_nhds

added theorem is_bounded_le_nhds

added theorem is_cobounded_ge_nhds

added theorem is_cobounded_le_nhds

added theorem le_nhds_of_Limsup_eq_Liminf

added theorem lt_mem_sets_of_Limsup_lt

added theorem tendsto_of_le_liminf_of_limsup_le

added theorem tendsto_of_liminf_eq_limsup

Modified src/topology/algebra/ordered/proj_Icc.lean

Modified src/topology/continuous_function/basic.lean

Renamed src/topology/extend_from_subset.lean to src/topology/extend_from.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/topological_fiber_bundle.lean