Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 19:43 34d8ff1d

View on Github →

feat(topology/algebra/weak_dual): generalize to weak topologies for arbitrary dualities (#12284)

Estimated changes

added theorem bilin_embedding
added theorem coe_fn_continuous
added theorem dual_pairing_apply
added theorem eval_continuous
added def top_dual_pairing
added def weak_bilin
deleted theorem weak_dual.eval_continuous
modified def weak_dual
added def weak_space