Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-05-15 13:26
136e67a6
View on Github →
refactor(topology): change continuous_at_within to continuous_within_at (
#1034
)
Estimated changes
Modified
src/analysis/normed_space/deriv.lean
deleted
theorem
differentiable_within_at.continuous_at_within
added
theorem
differentiable_within_at.continuous_within_at
deleted
theorem
has_fderiv_within_at.continuous_at_within
added
theorem
has_fderiv_within_at.continuous_within_at
Modified
src/topology/basic.lean
deleted
def
continuous_at_within
modified
def
continuous_on
added
def
continuous_within_at
Modified
src/topology/constructions.lean
deleted
theorem
continuous_at_within.prod
added
theorem
continuous_within_at.prod
Modified
src/topology/order.lean
deleted
theorem
continuous_at.continuous_at_within
added
theorem
continuous_at.continuous_within_at
deleted
theorem
continuous_at_within.mono
deleted
theorem
continuous_at_within.tendsto_nhds_within_image
deleted
theorem
continuous_at_within_iff_continuous_at_restrict
deleted
theorem
continuous_at_within_iff_ptendsto_res
deleted
theorem
continuous_at_within_univ
added
theorem
continuous_within_at.mono
added
theorem
continuous_within_at.tendsto_nhds_within_image
added
theorem
continuous_within_at_iff_continuous_at_restrict
added
theorem
continuous_within_at_iff_ptendsto_res
added
theorem
continuous_within_at_univ
modified
theorem
nhds_within_le_comap