Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-15 02:59 b7d980c5

View on Github →

feat(topology/algebra/weak_dual_topology + analysis/normed_space/weak_dual_of_normed_space): add definition and first lemmas about weak-star topology (#8598) Add definition and first lemmas about weak-star topology.

Estimated changes

Created src/analysis/normed_space/weak_dual.lean

added def normed_space.dual.continuous_linear_map_to_weak_dual

added theorem normed_space.dual.dual_norm_topology_le_weak_dual_topology

added def normed_space.dual.to_weak_dual

added theorem normed_space.dual.to_weak_dual_continuous

added theorem normed_space.dual.to_weak_dual_eq_iff

added theorem weak_dual.coe_to_fun_eq_normed_coe_to_fun

added def weak_dual.to_normed_dual

added theorem weak_dual.to_normed_dual_eq_iff

Created src/topology/algebra/weak_dual_topology.lean

added theorem weak_dual.coe_fn_continuous

added theorem weak_dual.continuous_of_continuous_eval

added theorem weak_dual.eval_continuous

added theorem weak_dual.tendsto_iff_forall_eval_tendsto

added def weak_dual