Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-02 10:40 033ecbfd

View on Github →

chore(topology/*): add a few more trivial continuous_(within_)at lemmas (#1842)

Estimated changes

Modified src/topology/algebra/group.lean

added theorem continuous_at.inv

added theorem continuous_within_at.inv

Modified src/topology/algebra/monoid.lean

added theorem continuous_at.mul

added theorem continuous_within_at.mul

Modified src/topology/basic.lean

added theorem continuous_at_const

added theorem continuous_at_id

Modified src/topology/continuous_on.lean

added theorem continuous_on_id

added theorem continuous_within_at_const

added theorem continuous_within_at_id