Commit 2023-04-26 04:57 39ecb3bb

View on Github →

feat: port Analysis.Seminorm (#3484)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Seminorm.lean

added theorem Seminorm.add_apply

added theorem Seminorm.add_comp

added theorem Seminorm.balanced_ball_zero

added theorem Seminorm.balanced_closedBall_zero

added def Seminorm.ball

added theorem Seminorm.ball_add_ball_subset

added theorem Seminorm.ball_antitone

added theorem Seminorm.ball_bot

added theorem Seminorm.ball_comp

added theorem Seminorm.ball_eq_emptyset

added theorem Seminorm.ball_finset_sup'

added theorem Seminorm.ball_finset_sup

added theorem Seminorm.ball_finset_sup_eq_interᵢ

added theorem Seminorm.ball_mono

added theorem Seminorm.ball_norm_mul_subset

added theorem Seminorm.ball_smul

added theorem Seminorm.ball_smul_ball

added theorem Seminorm.ball_subset_closedBall

added theorem Seminorm.ball_sup

added theorem Seminorm.ball_zero'

added theorem Seminorm.ball_zero_absorbs_ball_zero

added theorem Seminorm.ball_zero_eq

added theorem Seminorm.ball_zero_eq_preimage_ball

added theorem Seminorm.bddBelow_range_add

added theorem Seminorm.bot_eq_zero

added def Seminorm.closedBall

added theorem Seminorm.closedBall_add_closedBall_subset

added theorem Seminorm.closedBall_antitone

added theorem Seminorm.closedBall_bot

added theorem Seminorm.closedBall_comp

added theorem Seminorm.closedBall_eq_binterᵢ_ball

added theorem Seminorm.closedBall_eq_emptyset

added theorem Seminorm.closedBall_finset_sup'

added theorem Seminorm.closedBall_finset_sup

added theorem Seminorm.closedBall_finset_sup_eq_interᵢ

added theorem Seminorm.closedBall_mono

added theorem Seminorm.closedBall_smul

added theorem Seminorm.closedBall_smul_closedBall

added theorem Seminorm.closedBall_sup

added theorem Seminorm.closedBall_zero'

added theorem Seminorm.closedBall_zero_eq

added theorem Seminorm.closedBall_zero_eq_preimage_closedBall

added def Seminorm.coeFnAddMonoidHom

added theorem Seminorm.coeFnAddMonoidHom_injective

added theorem Seminorm.coe_add

added theorem Seminorm.coe_bot

added theorem Seminorm.coe_comp

added theorem Seminorm.coe_le_coe

added theorem Seminorm.coe_lt_coe

added theorem Seminorm.coe_restrictScalars

added theorem Seminorm.coe_smul

added theorem Seminorm.coe_sup

added theorem Seminorm.coe_zero

added def Seminorm.comp

added theorem Seminorm.comp_add_le

added theorem Seminorm.comp_apply

added theorem Seminorm.comp_comp

added theorem Seminorm.comp_id

added theorem Seminorm.comp_mono

added theorem Seminorm.comp_smul

added theorem Seminorm.comp_smul_apply

added theorem Seminorm.comp_zero

added theorem Seminorm.continuousAt_zero'

added theorem Seminorm.continuousAt_zero

added theorem Seminorm.continuous_of_le

added theorem Seminorm.convex_ball

added theorem Seminorm.convex_closedBall

added theorem Seminorm.ext

added theorem Seminorm.finset_sup_apply

added theorem Seminorm.finset_sup_apply_le

added theorem Seminorm.finset_sup_apply_lt

added theorem Seminorm.finset_sup_le_sum

added theorem Seminorm.inf_apply

added theorem Seminorm.le_def

added theorem Seminorm.lt_def

added theorem Seminorm.mem_ball

added theorem Seminorm.mem_ball_self

added theorem Seminorm.mem_ball_zero

added theorem Seminorm.mem_closedBall

added theorem Seminorm.mem_closedBall_self

added theorem Seminorm.mem_closedBall_zero

added theorem Seminorm.neg_ball

added theorem Seminorm.norm_sub_map_le_sub

added def Seminorm.of

added def Seminorm.ofSmulLe

added theorem Seminorm.preimage_metric_ball

added theorem Seminorm.preimage_metric_closedBall

added def Seminorm.pullback

added theorem Seminorm.restrictScalars_ball

added theorem Seminorm.restrictScalars_closedBall

added theorem Seminorm.smul_apply

added theorem Seminorm.smul_ball_preimage

added theorem Seminorm.smul_ball_zero

added theorem Seminorm.smul_closedBall_subset

added theorem Seminorm.smul_closedBall_zero

added theorem Seminorm.smul_comp

added theorem Seminorm.smul_inf

added theorem Seminorm.smul_le_smul

added theorem Seminorm.smul_sup

added theorem Seminorm.sub_mem_ball

added theorem Seminorm.sup_apply

added theorem Seminorm.symmetric_ball_zero

added theorem Seminorm.vadd_ball

added theorem Seminorm.vadd_closedBall

added theorem Seminorm.zero_apply

added theorem Seminorm.zero_comp

added structure Seminorm

added theorem absorbent_ball

added theorem absorbent_ball_zero

added theorem balanced_ball_zero

added theorem ball_normSeminorm

added theorem coe_normSeminorm

added def normSeminorm

Modified Mathlib/Lean/Meta.lean