Commit 2025-03-12 03:44 4326b6f8
View on Github →feat(Topology/): add Submodule.closure_coe_iSup_map_single (#22752)
I'm going to use this lemma to prove UniqueDiffWithinAt.pi
without assuming that the index type is finite,
as a part of generalizing the file to TVS.
Also add ContinuousLinearMap.single
and generalize le_comap_single_pi
from Submodule.pi Set.univ _ to .pi I _.