Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-03 22:24 ec839ef0

View on Github →

feat(topology/algebra/order): continuity of monotone functions (#5199) Add local versions of order_iso.continuous.

Estimated changes

Modified src/topology/algebra/ordered.lean

added theorem continuous_at_left_of_mono_incr_on_of_closure_image_mem_nhds_within

added theorem continuous_at_left_of_mono_incr_on_of_exists_between

added theorem continuous_at_left_of_mono_incr_on_of_image_mem_nhds_within

added theorem continuous_at_of_mono_incr_on_of_closure_image_mem_nhds

added theorem continuous_at_of_mono_incr_on_of_exists_between

added theorem continuous_at_of_mono_incr_on_of_image_mem_nhds

added theorem continuous_at_right_of_mono_incr_on_of_closure_image_mem_nhds_within

added theorem continuous_at_right_of_mono_incr_on_of_exists_between

added theorem continuous_at_right_of_mono_incr_on_of_image_mem_nhds_within

added theorem monotone.continuous_of_dense_range

added theorem monotone.continuous_of_surjective

added theorem strict_mono_incr_on.continuous_at_left_of_closure_image_mem_nhds_within

added theorem strict_mono_incr_on.continuous_at_left_of_exists_between

added theorem strict_mono_incr_on.continuous_at_left_of_image_mem_nhds_within

added theorem strict_mono_incr_on.continuous_at_left_of_surj_on

added theorem strict_mono_incr_on.continuous_at_of_closure_image_mem_nhds

added theorem strict_mono_incr_on.continuous_at_of_exists_between

added theorem strict_mono_incr_on.continuous_at_of_image_mem_nhds

added theorem strict_mono_incr_on.continuous_at_right_of_closure_image_mem_nhds_within

added theorem strict_mono_incr_on.continuous_at_right_of_exists_between

added theorem strict_mono_incr_on.continuous_at_right_of_image_mem_nhds_within

added theorem strict_mono_incr_on.continuous_at_right_of_surj_on