Commit 2025-02-26 21:00 068c55c5

View on Github →

feature(Analysis/Seminorm): Add closedBall equivalents of open ball results (#22264) Adds closedBall equivalents of existing (open) ball results. Specifically:

sub_mem_closedBall
neg_mem_closedBall_zero
neg_closedBall
smul_closedBall_preimage
closedBall_normSeminorm
blanced_closedBall_zero balanced_closedBall_zero is used in #21002

Estimated changes

Modified Mathlib/Analysis/Seminorm.lean

added theorem Seminorm.neg_closedBall

added theorem Seminorm.neg_mem_closedBall_zero

added theorem Seminorm.smul_closedBall_preimage

added theorem Seminorm.sub_mem_closedBall

added theorem balanced_closedBall_zero

added theorem closedBall_normSeminorm