Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 20:59 a990661d

View on Github →

feat(analysis/[seminorm, locally_convex/with_seminorms]): semilinearize seminorm.comp (#17286)

Estimated changes

Modified src/analysis/locally_convex/with_seminorms.lean

modified theorem inducing.with_seminorms

modified theorem linear_map.with_seminorms_induced

modified theorem seminorm.cont_with_seminorms_normed_space

modified theorem seminorm.continuous_from_bounded

modified theorem seminorm.continuous_iff_continuous_comp

modified theorem seminorm.continuous_of_continuous_comp

modified def seminorm.is_bounded

modified theorem seminorm.is_bounded_sup

modified def seminorm_family.comp

modified theorem seminorm_family.comp_apply

modified theorem seminorm_family.finset_sup_comp

Modified src/analysis/seminorm.lean

modified theorem seminorm.add_comp

modified theorem seminorm.ball_comp

modified theorem seminorm.closed_ball_comp

modified theorem seminorm.coe_comp

modified def seminorm.comp

modified theorem seminorm.comp_add_le

modified theorem seminorm.comp_apply

modified theorem seminorm.comp_comp

modified theorem seminorm.comp_mono

modified theorem seminorm.comp_smul

modified theorem seminorm.comp_smul_apply

modified theorem seminorm.comp_zero

modified def seminorm.pullback

modified theorem seminorm.smul_comp

modified theorem seminorm.zero_comp