Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 13:18 41b56455

View on Github →

chore(topology/algebra/ordered/basic): move code out of basic (#9772)

Estimated changes

Modified src/data/real/sqrt.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/topology/algebra/group.lean

added theorem tendsto_inv_nhds_within_Ici

added theorem tendsto_inv_nhds_within_Ici_inv

added theorem tendsto_inv_nhds_within_Iic

added theorem tendsto_inv_nhds_within_Iic_inv

added theorem tendsto_inv_nhds_within_Iio

added theorem tendsto_inv_nhds_within_Iio_inv

added theorem tendsto_inv_nhds_within_Ioi

added theorem tendsto_inv_nhds_within_Ioi_inv

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

deleted theorem continuous.exists_forall_ge

deleted theorem continuous.exists_forall_le

deleted theorem continuous_at_iff_continuous_left'_right'

deleted theorem continuous_at_iff_continuous_left_right

deleted theorem continuous_at_left_of_monotone_on_of_closure_image_mem_nhds_within

deleted theorem continuous_at_left_of_monotone_on_of_exists_between

deleted theorem continuous_at_left_of_monotone_on_of_image_mem_nhds_within

deleted theorem continuous_at_of_monotone_on_of_closure_image_mem_nhds

deleted theorem continuous_at_of_monotone_on_of_exists_between

deleted theorem continuous_at_of_monotone_on_of_image_mem_nhds

deleted theorem continuous_at_right_of_monotone_on_of_closure_image_mem_nhds_within

deleted theorem continuous_at_right_of_monotone_on_of_exists_between

deleted theorem continuous_at_right_of_monotone_on_of_image_mem_nhds_within

deleted theorem continuous_within_at_Iio_iff_Iic

deleted theorem continuous_within_at_Ioi_iff_Ici

deleted theorem eq_Icc_of_connected_compact

deleted theorem is_compact.Inf_mem

deleted theorem is_compact.Sup_mem

deleted theorem is_compact.exists_Inf_image_eq

deleted theorem is_compact.exists_Sup_image_eq

deleted theorem is_compact.exists_forall_ge

deleted theorem is_compact.exists_forall_le

deleted theorem is_compact.exists_is_glb

deleted theorem is_compact.exists_is_greatest

deleted theorem is_compact.exists_is_least

deleted theorem is_compact.exists_is_lub

deleted theorem is_compact.is_glb_Inf

deleted theorem is_compact.is_greatest_Sup

deleted theorem is_compact.is_least_Inf

deleted theorem is_compact.is_lub_Sup

deleted theorem is_compact_Icc

deleted theorem is_compact_interval

deleted theorem is_compact_pi_Icc

deleted theorem monotone.continuous_of_dense_range

deleted theorem monotone.continuous_of_surjective

deleted theorem nhds_left'_sup_nhds_right

deleted theorem nhds_left_sup_nhds_right'

deleted theorem nhds_left_sup_nhds_right

deleted theorem order_iso.coe_to_homeomorph

deleted theorem order_iso.coe_to_homeomorph_symm

deleted def order_iso.to_homeomorph

deleted theorem strict_mono_on.continuous_at_left_of_closure_image_mem_nhds_within

deleted theorem strict_mono_on.continuous_at_left_of_exists_between

deleted theorem strict_mono_on.continuous_at_left_of_image_mem_nhds_within

deleted theorem strict_mono_on.continuous_at_left_of_surj_on

deleted theorem strict_mono_on.continuous_at_of_closure_image_mem_nhds

deleted theorem strict_mono_on.continuous_at_of_exists_between

deleted theorem strict_mono_on.continuous_at_of_image_mem_nhds

deleted theorem strict_mono_on.continuous_at_right_of_closure_image_mem_nhds_within

deleted theorem strict_mono_on.continuous_at_right_of_exists_between

deleted theorem strict_mono_on.continuous_at_right_of_image_mem_nhds_within

deleted theorem strict_mono_on.continuous_at_right_of_surj_on

deleted theorem tendsto_inv_nhds_within_Ici

deleted theorem tendsto_inv_nhds_within_Ici_inv

deleted theorem tendsto_inv_nhds_within_Iic

deleted theorem tendsto_inv_nhds_within_Iic_inv

deleted theorem tendsto_inv_nhds_within_Iio

deleted theorem tendsto_inv_nhds_within_Iio_inv

deleted theorem tendsto_inv_nhds_within_Ioi

deleted theorem tendsto_inv_nhds_within_Ioi_inv

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

added theorem continuous.exists_forall_ge

added theorem continuous.exists_forall_le

added theorem eq_Icc_of_connected_compact

added theorem is_compact.Inf_mem

added theorem is_compact.Sup_mem

added theorem is_compact.exists_Inf_image_eq

added theorem is_compact.exists_Sup_image_eq

added theorem is_compact.exists_forall_ge

added theorem is_compact.exists_forall_le

added theorem is_compact.exists_is_glb

added theorem is_compact.exists_is_greatest

added theorem is_compact.exists_is_least

added theorem is_compact.exists_is_lub

added theorem is_compact.is_glb_Inf

added theorem is_compact.is_greatest_Sup

added theorem is_compact.is_least_Inf

added theorem is_compact.is_lub_Sup

added theorem is_compact_Icc

added theorem is_compact_interval

added theorem is_compact_pi_Icc

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

added theorem continuous_at_iff_continuous_left'_right'

added theorem continuous_at_iff_continuous_left_right

added theorem continuous_within_at_Iio_iff_Iic

added theorem continuous_within_at_Ioi_iff_Ici

added theorem nhds_left'_sup_nhds_right

added theorem nhds_left_sup_nhds_right'

added theorem nhds_left_sup_nhds_right

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

added theorem continuous_at_left_of_monotone_on_of_closure_image_mem_nhds_within

added theorem continuous_at_left_of_monotone_on_of_exists_between

added theorem continuous_at_left_of_monotone_on_of_image_mem_nhds_within

added theorem continuous_at_of_monotone_on_of_closure_image_mem_nhds

added theorem continuous_at_of_monotone_on_of_exists_between

added theorem continuous_at_of_monotone_on_of_image_mem_nhds

added theorem continuous_at_right_of_monotone_on_of_closure_image_mem_nhds_within

added theorem continuous_at_right_of_monotone_on_of_exists_between

added theorem continuous_at_right_of_monotone_on_of_image_mem_nhds_within

added theorem monotone.continuous_of_dense_range

added theorem monotone.continuous_of_surjective

added theorem order_iso.coe_to_homeomorph

added theorem order_iso.coe_to_homeomorph_symm

added def order_iso.to_homeomorph

added theorem strict_mono_on.continuous_at_left_of_closure_image_mem_nhds_within

added theorem strict_mono_on.continuous_at_left_of_exists_between

added theorem strict_mono_on.continuous_at_left_of_image_mem_nhds_within

added theorem strict_mono_on.continuous_at_left_of_surj_on

added theorem strict_mono_on.continuous_at_of_closure_image_mem_nhds

added theorem strict_mono_on.continuous_at_of_exists_between

added theorem strict_mono_on.continuous_at_of_image_mem_nhds

added theorem strict_mono_on.continuous_at_right_of_closure_image_mem_nhds_within

added theorem strict_mono_on.continuous_at_right_of_exists_between

added theorem strict_mono_on.continuous_at_right_of_image_mem_nhds_within

added theorem strict_mono_on.continuous_at_right_of_surj_on

Modified src/topology/instances/ereal.lean

Modified src/topology/metric_space/basic.lean