Commit 2023-04-10 13:06 00f16170

View on Github →

feat: port Topology.Algebra.Module.WeakDual (#3366)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Module/WeakDual.lean

added theorem WeakBilin.coeFn_continuous

added theorem WeakBilin.continuous_of_continuous_eval

added theorem WeakBilin.embedding

added theorem WeakBilin.eval_continuous

added theorem WeakBilin.tendsto_iff_forall_eval_tendsto

added def WeakBilin

added theorem WeakDual.coeFn_continuous

added theorem WeakDual.continuous_of_continuous_eval

added theorem WeakDual.eval_continuous

added def WeakDual

added theorem WeakSpace.coe_map

added def WeakSpace.map

added theorem WeakSpace.map_apply

added def WeakSpace

added theorem tendsto_iff_forall_eval_tendsto_topDualPairing

added def topDualPairing

added theorem topDualPairing_apply