Commit 2023-05-25 08:46 24e633e9

View on Github →

feat: port Analysis.NormedSpace.Dual (#4310)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Dual.lean

added def NormedSpace.Dual

added theorem NormedSpace.bounded_polar_of_mem_nhds_zero

added theorem NormedSpace.closedBall_inv_subset_polar_closedBall

added theorem NormedSpace.double_dual_bound

added def NormedSpace.dualPairing

added theorem NormedSpace.dualPairing_apply

added theorem NormedSpace.dualPairing_separatingLeft

added theorem NormedSpace.dual_def

added theorem NormedSpace.eq_iff_forall_dual_eq

added theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero

added theorem NormedSpace.eq_zero_of_forall_dual_eq_zero

added def NormedSpace.inclusionInDoubleDual

added def NormedSpace.inclusionInDoubleDualLi

added theorem NormedSpace.inclusionInDoubleDual_norm_eq

added theorem NormedSpace.inclusionInDoubleDual_norm_le

added theorem NormedSpace.isClosed_polar

added theorem NormedSpace.mem_polar_iff

added theorem NormedSpace.norm_le_dual_bound

added def NormedSpace.polar

added theorem NormedSpace.polar_ball_subset_closedBall_div

added theorem NormedSpace.polar_closedBall

added theorem NormedSpace.polar_closure

added theorem NormedSpace.polar_univ

added theorem NormedSpace.smul_mem_polar