Commit 2024-02-08 16:52 faecefeb

View on Github →

feat(Algebra/UniformConvergence): drop unneeded assumptions (#10321)

Prove a version of UniformOnFun.continuousSMul_induced_of_image_bounded for UniformFuns.
Deal with φ : H →ₗ[𝕜] (α → E) and ofFun ∘ φ, not φ : H →ₗ[𝕜] (α →ᵤ[𝔖] E).
Drop unneeded assumptions (nonempty, directed).

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

added theorem Absorbs.eventually_nhds_zero

added theorem absorbs_iff_eventually_nhdsWithin_zero

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

added theorem UniformFun.continuousSMul_induced_of_range_bounded

modified theorem UniformOnFun.continuousSMul_induced_of_image_bounded

modified theorem UniformOnFun.continuousSMul_submodule_of_image_bounded

Modified Mathlib/Topology/Order.lean

modified theorem induced_compose