Commit 2023-01-31 21:41 195bf2a1

View on Github →

feat: port Topology.ContinuousOn (#1907)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Constructions.lean

deleted theorem map_nhds_subtype_coe_eq

added theorem map_nhds_subtype_coe_eq_nhds

added theorem map_nhds_subtype_val

Created Mathlib/Topology/ContinuousOn.lean

added theorem Continuous.comp_continuousOn

added theorem Continuous.continuousOn

added theorem Continuous.continuousWithinAt

added theorem Continuous.if

added theorem Continuous.if_const

added theorem Continuous.piecewise

added theorem ContinuousAt.comp_continuousWithinAt

added theorem ContinuousAt.continuousOn

added theorem ContinuousAt.continuousWithinAt

added theorem ContinuousOn.comp'

added theorem ContinuousOn.comp

added theorem ContinuousOn.comp_continuous

added theorem ContinuousOn.congr

added theorem ContinuousOn.congr_mono

added theorem ContinuousOn.continuousAt

added theorem ContinuousOn.continuousWithinAt

added theorem ContinuousOn.fst

added theorem ContinuousOn.if'

added theorem ContinuousOn.if

added theorem ContinuousOn.image_closure

added theorem ContinuousOn.isOpen_preimage

added theorem ContinuousOn.mono

added theorem ContinuousOn.mono_dom

added theorem ContinuousOn.mono_rng

added theorem ContinuousOn.piecewise'

added theorem ContinuousOn.piecewise

added theorem ContinuousOn.preimage_closed_of_closed

added theorem ContinuousOn.preimage_interior_subset_interior_preimage

added theorem ContinuousOn.preimage_open_of_open

added theorem ContinuousOn.prod

added theorem ContinuousOn.prod_map

added theorem ContinuousOn.snd

added def ContinuousOn

added theorem ContinuousWithinAt.comp'

added theorem ContinuousWithinAt.comp

added theorem ContinuousWithinAt.congr

added theorem ContinuousWithinAt.congr_mono

added theorem ContinuousWithinAt.congr_of_eventuallyEq

added theorem ContinuousWithinAt.continuousAt

added theorem ContinuousWithinAt.diff_iff

added theorem ContinuousWithinAt.fin_insertNth

added theorem ContinuousWithinAt.fst

added theorem ContinuousWithinAt.image_closure

added theorem ContinuousWithinAt.mem_closure

added theorem ContinuousWithinAt.mem_closure_image

added theorem ContinuousWithinAt.mono

added theorem ContinuousWithinAt.mono_of_mem

added theorem ContinuousWithinAt.preimage_mem_nhdsWithin

added theorem ContinuousWithinAt.preimage_mem_nhds_within'

added theorem ContinuousWithinAt.prod

added theorem ContinuousWithinAt.prod_map

added theorem ContinuousWithinAt.snd

added theorem ContinuousWithinAt.tendsto

added theorem ContinuousWithinAt.tendsto_nhdsWithin

added theorem ContinuousWithinAt.tendsto_nhdsWithin_image

added theorem ContinuousWithinAt.union

added def ContinuousWithinAt

added theorem DenseRange.nhdsWithin_neBot

added theorem Embedding.continuousOn_iff

added theorem Embedding.map_nhdsWithin_eq

added theorem Filter.Eventually.self_of_nhdsWithin

added theorem Filter.EventuallyEq.congr_continuousWithinAt

added theorem Filter.EventuallyEq.eq_of_nhdsWithin

added theorem Filter.Tendsto.if_nhdsWithin

added theorem Filter.Tendsto.piecewise_nhdsWithin

added theorem Function.LeftInverse.map_nhds_eq

added theorem Inducing.continuousOn_iff

added theorem Inducing.continuousWithinAt_iff

added theorem IsClosed.mem_of_nhdsWithin_neBot

added theorem IsOpen.continuousOn_iff

added theorem IsOpen.ite'

added theorem IsOpen.ite

added theorem IsOpen.nhdsWithin_eq

added theorem IsOpenMap.continuousOn_image_of_leftInvOn

added theorem IsOpenMap.continuousOn_range_of_leftInverse

added theorem OpenEmbedding.map_nhdsWithin_preimage_eq

added theorem Set.EqOn.eventuallyEq_nhdsWithin

added theorem Set.LeftInvOn.map_nhdsWithin_eq

added theorem Set.MapsTo.closure_of_continuousOn

added theorem Set.MapsTo.closure_of_continuousWithinAt

added theorem Set.Subsingleton.continuousOn

added theorem antitone_continuousOn

added theorem closure_pi_set

added theorem comap_nhdsWithin_range

added theorem continuousAt_update_same

added theorem continuousOn_congr

added theorem continuousOn_const

added theorem continuousOn_empty

added theorem continuousOn_fst

added theorem continuousOn_id

added theorem continuousOn_iff'

added theorem continuousOn_iff

added theorem continuousOn_iff_continuous_restrict

added theorem continuousOn_iff_isClosed

added theorem continuousOn_of_locally_continuousOn

added theorem continuousOn_open_iff

added theorem continuousOn_open_of_generateFrom

added theorem continuousOn_pi

added theorem continuousOn_piecewise_ite'

added theorem continuousOn_piecewise_ite

added theorem continuousOn_singleton

added theorem continuousOn_snd

added theorem continuousOn_to_generateFrom_iff

added theorem continuousWithinAt_compl_self

added theorem continuousWithinAt_const

added theorem continuousWithinAt_diff_self

added theorem continuousWithinAt_fst

added theorem continuousWithinAt_id

added theorem continuousWithinAt_iff_continuousAt

added theorem continuousWithinAt_iff_continuousAt_restrict

added theorem continuousWithinAt_insert_self

added theorem continuousWithinAt_inter'

added theorem continuousWithinAt_inter

added theorem continuousWithinAt_of_not_mem_closure

added theorem continuousWithinAt_pi

added theorem continuousWithinAt_prod_iff

added theorem continuousWithinAt_singleton

added theorem continuousWithinAt_snd

added theorem continuousWithinAt_union

added theorem continuousWithinAt_univ

added theorem continuousWithinAt_update_same

added theorem continuous_if'

added theorem continuous_if

added theorem continuous_if_const

added theorem continuous_iff_continuousOn_univ

added theorem continuous_piecewise

added theorem dense_pi

added theorem diff_mem_nhdsWithin_compl

added theorem diff_mem_nhdsWithin_diff

added theorem eventuallyEq_nhdsWithin_iff

added theorem eventuallyEq_nhdsWithin_of_eqOn

added theorem eventually_mem_nhdsWithin

added theorem eventually_mem_of_tendsto_nhdsWithin

added theorem eventually_nhdsWithin_iff

added theorem eventually_nhdsWithin_nhdsWithin

added theorem eventually_nhdsWithin_of_eventually_nhds

added theorem eventually_nhdsWithin_of_forall

added theorem eventually_nhds_nhdsWithin

added theorem frequently_nhdsWithin_iff

added theorem frontier_inter_open_inter

added theorem insert_mem_nhdsWithin_insert

added theorem insert_mem_nhds_iff

added theorem inter_mem_nhdsWithin

added theorem ite_inter_closure_compl_eq_of_inter_frontier_eq

added theorem ite_inter_closure_eq_of_inter_frontier_eq

added theorem map_nhdsWithin

added theorem mem_closure_ne_iff_frequently_within

added theorem mem_closure_pi

added theorem mem_nhdsWithin

added theorem mem_nhdsWithin_iff_eventually

added theorem mem_nhdsWithin_iff_eventuallyEq

added theorem mem_nhdsWithin_iff_exists_mem_nhds_inter

added theorem mem_nhdsWithin_insert

added theorem mem_nhdsWithin_of_mem_nhds

added theorem mem_nhdsWithin_subtype

added theorem mem_nhds_subtype_iff_nhdsWithin

added theorem mem_of_mem_nhdsWithin

added theorem nhdsWithin_basis_open

added theorem nhdsWithin_compl_singleton_sup_pure

added theorem nhdsWithin_empty

added theorem nhdsWithin_eq

added theorem nhdsWithin_eq_iff_eventuallyEq

added theorem nhdsWithin_eq_map_subtype_coe

added theorem nhdsWithin_eq_nhdsWithin

added theorem nhdsWithin_eq_nhds_within'

added theorem nhdsWithin_hasBasis

added theorem nhdsWithin_insert

added theorem nhdsWithin_inter'

added theorem nhdsWithin_inter

added theorem nhdsWithin_inter_of_mem

added theorem nhdsWithin_le_comap

added theorem nhdsWithin_le_iff

added theorem nhdsWithin_le_nhds

added theorem nhdsWithin_le_of_mem

added theorem nhdsWithin_mono

added theorem nhdsWithin_neBot_of_mem

added theorem nhdsWithin_pi_eq'

added theorem nhdsWithin_pi_eq

added theorem nhdsWithin_pi_eq_bot

added theorem nhdsWithin_pi_neBot

added theorem nhdsWithin_pi_univ_eq

added theorem nhdsWithin_prod

added theorem nhdsWithin_restrict''

added theorem nhdsWithin_restrict'

added theorem nhdsWithin_restrict

added theorem nhdsWithin_singleton

added theorem nhdsWithin_subtype

added theorem nhdsWithin_union

added theorem nhdsWithin_univ

added theorem nhds_bind_nhdsWithin

added theorem nhds_of_nhdsWithin_of_nhds

added theorem preimage_coe_mem_nhds_subtype

added theorem preimage_nhdsWithin_coinduced'

added theorem preimage_nhds_within_coinduced

added theorem principal_subtype

added theorem pure_le_nhdsWithin

added theorem self_mem_nhdsWithin

added theorem tendsto_const_nhdsWithin

added theorem tendsto_nhdsWithin_congr

added theorem tendsto_nhdsWithin_iff

added theorem tendsto_nhdsWithin_iff_subtype

added theorem tendsto_nhdsWithin_mono_left

added theorem tendsto_nhdsWithin_mono_right

added theorem tendsto_nhdsWithin_of_tendsto_nhds

added theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within

added theorem tendsto_nhdsWithin_range

added theorem tendsto_nhds_of_tendsto_nhdsWithin