Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-18 16:04 470ddbdb

View on Github →

chore(analysis,topology): add missing ulift instances (#14217)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem ulift.algebra_map_eq

added theorem ulift.down_algebra_map

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

added theorem ulift.nnnorm_def

added theorem ulift.nnnorm_up

added theorem ulift.norm_def

added theorem ulift.norm_up

Modified src/analysis/normed/normed_field.lean

Modified src/analysis/normed_space/basic.lean

Modified src/topology/metric_space/basic.lean

added theorem ulift.dist_eq

added theorem ulift.dist_up_up

added theorem ulift.nndist_eq

added theorem ulift.nndist_up_up

Modified src/topology/metric_space/emetric_space.lean

added theorem ulift.edist_eq

added theorem ulift.edist_up_up