Commit 2023-12-20 23:32 56ce93a6
View on Github →chore(UniformConvergenceTopology): use variable
, fix types (#9132)
- Use
variable
. - Add
toFun
/ofFun
to abuse the definitional equality less often. - Review instances in
Topology.Algebra.UniformConvergence
. - Replace
*_apply
lemmas withtoFun_*
/ofFun_*
lemmas.