Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-20 08:30 a35d6824

View on Github →

feat(topology/order): more facts on continuous_on (#1140)

Estimated changes

Modified src/topology/algebra/group.lean

added theorem continuous_on.inv

added theorem continuous_on.sub

Modified src/topology/algebra/monoid.lean

added theorem continuous_on.mul

Modified src/topology/basic.lean

added theorem nhds_within_le_of_mem

added theorem nhds_within_restrict''

added theorem self_mem_nhds_within

Modified src/topology/order.lean

added theorem continuous.comp_continuous_on

added theorem continuous.continuous_at

added theorem continuous_at.preimage_mem_nhds

added theorem continuous_on.preimage_closed_of_closed

added theorem continuous_on_iff_is_closed

added theorem continuous_on_open_iff

added theorem continuous_on_open_of_generate_from

added theorem continuous_within_at.congr_of_mem_nhds_within

added theorem continuous_within_at.continuous_at

added theorem continuous_within_at.preimage_mem_nhds_within

added theorem continuous_within_at_inter'

added theorem continuous_within_at_inter