Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 12:36 3339976e

View on Github →

refactor(topology/constructions): rename continuous_subtype_mk (#16223)

rename continuous_subtype_mk to continuous.subtype_mk to allow dot notation;
add continuous.subtype_map.

Estimated changes

Modified src/algebraic_topology/topological_simplex.lean

Modified src/analysis/convex/contractible.lean

Modified src/analysis/normed/field/unit_ball.lean

Modified src/analysis/normed/group/ball_sphere.lean

Modified src/analysis/normed/group/basic.lean

modified theorem continuous_norm

Modified src/analysis/normed_space/ball_action.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/special_functions/exp.lean

Modified src/analysis/special_functions/log/basic.lean

Modified src/dynamics/flow.lean

Modified src/geometry/manifold/instances/real.lean

Modified src/topology/algebra/module/basic.lean

Modified src/topology/algebra/order/proj_Icc.lean

Modified src/topology/algebra/semigroup.lean

Modified src/topology/bases.lean

Modified src/topology/category/CompHaus/default.lean

Modified src/topology/constructions.lean

added theorem continuous.subtype_map

added theorem continuous.subtype_mk

deleted theorem continuous_subtype_mk

Modified src/topology/continuous_function/bounded.lean

Modified src/topology/homeomorph.lean

Modified src/topology/instances/ennreal.lean

Modified src/topology/instances/ereal.lean

Modified src/topology/instances/nnreal.lean

Modified src/topology/instances/real.lean

Modified src/topology/local_homeomorph.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/metric_space/pi_nat.lean

Modified src/topology/tietze_extension.lean

Modified src/topology/uniform_space/basic.lean

added theorem uniform_continuous.subtype_mk

deleted theorem uniform_continuous_subtype_mk

Modified src/topology/uniform_space/equiv.lean