Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-17 20:03 e5fc2a70

View on Github →

refactor(topology,calculus): change subset condition for composition (#1549)

refactor(topology,calculus): change subset condition for composition
improve docstrings
add is_open Ioi
reviewer's comments
typo

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem differentiable_on.congr

added theorem differentiable_within_at.congr

added theorem differentiable_within_at_inter'

modified theorem has_fderiv_within_at.comp

added theorem has_fderiv_within_at.image_tangent_cone_subset

added theorem has_fderiv_within_at.lim

added theorem has_fderiv_within_at.unique_diff_within_at

Modified src/analysis/calculus/mean_value.lean

Modified src/analysis/calculus/tangent_cone.lean

added theorem unique_diff_on.inter

deleted theorem unique_diff_on_inter

added theorem unique_diff_within_at.inter'

added theorem unique_diff_within_at_inter'

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/data/equiv/local_equiv.lean

Modified src/data/set/basic.lean

added theorem set.prod_range_univ_eq

added theorem set.prod_subset_preimage_fst

added theorem set.prod_subset_preimage_snd

added theorem set.prod_univ_range_eq

added theorem set.subset_preimage_univ

Modified src/geometry/manifold/manifold.lean

Modified src/topology/algebra/ordered.lean

added theorem is_open_Ioi

Modified src/topology/continuous_on.lean

added theorem continuous_on.congr

added theorem continuous_within_at.congr

added theorem continuous_within_at.mem_closure_image

added theorem continuous_within_at.preimage_mem_nhds_within'

added theorem mem_closure_iff_nhds_within_ne_bot

added theorem mem_nhds_within_of_mem_nhds

Modified src/topology/local_homeomorph.lean

added theorem local_homeomorph.continuous_at_iff_continuous_at_comp_left

added theorem local_homeomorph.continuous_at_iff_continuous_at_comp_right

added theorem local_homeomorph.continuous_at_inv_fun

added theorem local_homeomorph.continuous_at_to_fun

modified theorem local_homeomorph.continuous_on_iff_continuous_on_comp_left

added theorem local_homeomorph.continuous_within_at_iff_continuous_within_at_comp_left

added theorem local_homeomorph.continuous_within_at_iff_continuous_within_at_comp_right

added theorem local_homeomorph.image_open_of_open

added theorem local_homeomorph.to_homeomorph_inv_fun

added def local_homeomorph.to_homeomorph_of_source_eq_univ_target_eq_univ

added theorem local_homeomorph.to_homeomorph_to_fun