Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-08 13:51 afda1a2c

View on Github →

refactor(topology/continuous_on): move continuous_{on,within_at} to own file (#1516)

  • refactor(topology/continuous_on): move continuous_{on,within_at} to own file
  • Update src/topology/continuous_on.lean

Estimated changes

added theorem continuous_at.comp
deleted def continuous_on
deleted theorem inter_mem_nhds_within
deleted theorem map_nhds_within
deleted theorem mem_nhds_within
deleted def nhds_within
deleted theorem nhds_within_empty
deleted theorem nhds_within_eq
deleted theorem nhds_within_eq_of_open
deleted theorem nhds_within_inter'
deleted theorem nhds_within_inter
deleted theorem nhds_within_le_of_mem
deleted theorem nhds_within_mono
deleted theorem nhds_within_restrict''
deleted theorem nhds_within_restrict'
deleted theorem nhds_within_restrict
deleted theorem nhds_within_union
deleted theorem nhds_within_univ
deleted theorem self_mem_nhds_within
deleted theorem tendsto_if_nhds_within
deleted theorem continuous_on.prod
deleted theorem continuous_within_at.prod
added theorem continuous_on.comp
added theorem continuous_on.mono
added theorem continuous_on.prod
added def continuous_on
added theorem continuous_on_const
added theorem continuous_on_iff'
added theorem continuous_on_iff
added theorem continuous_on_open_iff
added theorem inter_mem_nhds_within
added theorem map_nhds_within
added theorem mem_nhds_within
added def nhds_within
added theorem nhds_within_empty
added theorem nhds_within_eq
added theorem nhds_within_eq_of_open
added theorem nhds_within_inter'
added theorem nhds_within_inter
added theorem nhds_within_le_comap
added theorem nhds_within_le_of_mem
added theorem nhds_within_mono
added theorem nhds_within_restrict''
added theorem nhds_within_restrict'
added theorem nhds_within_restrict
added theorem nhds_within_subtype
added theorem nhds_within_union
added theorem nhds_within_univ
added theorem principal_subtype
added theorem self_mem_nhds_within
added theorem tendsto_if_nhds_within
deleted theorem continuous.continuous_at
deleted theorem continuous.continuous_on
deleted theorem continuous_at.comp
deleted theorem continuous_on.comp
deleted theorem continuous_on.congr_mono
deleted theorem continuous_on.mono
deleted theorem continuous_on_const
deleted theorem continuous_on_iff'
deleted theorem continuous_on_iff
deleted theorem continuous_on_open_iff
deleted theorem continuous_within_at.comp
deleted theorem continuous_within_at.mono
deleted theorem continuous_within_at_univ
deleted theorem mem_nhds_within_subtype
deleted theorem nhds_within_le_comap
deleted theorem nhds_within_subtype
deleted theorem principal_subtype