Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 11:13 c03bd328

View on Github →

feat(analysis/normed_space/star): add lemmas about continuity and norm of identity (#11324)

Estimated changes

Modified src/analysis/normed_space/star.lean

added theorem continuous.star

added theorem continuous_at.star

added theorem continuous_at_star

added theorem continuous_on.star

added theorem continuous_on_star

added theorem continuous_star

added theorem continuous_within_at.star

added theorem continuous_within_at_star

added theorem cstar_ring.norm_one

modified theorem cstar_ring.norm_self_mul_star

modified theorem cstar_ring.norm_star_mul_self'

added theorem filter.tendsto.star

modified theorem star_isometry

modified def star_normed_group_hom

added theorem tendsto_star