Commit 2023-05-26 09:28 314bfe29

View on Github →

feat: port Analysis.NormedSpace.WeakDual (#4351)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/WeakDual.lean

added theorem NormedSpace.Dual.coe_toWeakDual

added def NormedSpace.Dual.continuousLinearMapToWeakDual

added theorem NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology

added theorem NormedSpace.Dual.isClosed_image_polar_of_mem_nhds

added def NormedSpace.Dual.toWeakDual

added theorem NormedSpace.Dual.toWeakDual_continuous

added theorem NormedSpace.Dual.toWeakDual_eq_iff

added theorem WeakDual.coe_toNormedDual

added theorem WeakDual.isClosed_closedBall

added theorem WeakDual.isClosed_image_coe_of_bounded_of_closed

added theorem WeakDual.isClosed_image_polar_of_mem_nhds

added theorem WeakDual.isClosed_polar

added theorem WeakDual.isCompact_closedBall

added theorem WeakDual.isCompact_of_bounded_of_closed

added theorem WeakDual.isCompact_polar

added def WeakDual.polar

added theorem WeakDual.polar_def

added def WeakDual.toNormedDual

added theorem WeakDual.toNormedDual_apply

added theorem WeakDual.toNormedDual_eq_iff