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 with toFun_*/ofFun_* lemmas.

Estimated changes

deleted theorem UniformFun.div_apply
deleted theorem UniformFun.inv_apply
deleted theorem UniformFun.mul_apply
added theorem UniformFun.ofFun_div
added theorem UniformFun.ofFun_inv
added theorem UniformFun.ofFun_mul
added theorem UniformFun.ofFun_one
added theorem UniformFun.ofFun_smul
deleted theorem UniformFun.one_apply
added theorem UniformFun.toFun_div
added theorem UniformFun.toFun_inv
added theorem UniformFun.toFun_mul
added theorem UniformFun.toFun_one
added theorem UniformFun.toFun_smul
deleted theorem UniformOnFun.div_apply
deleted theorem UniformOnFun.inv_apply
deleted theorem UniformOnFun.mul_apply
added theorem UniformOnFun.ofFun_div
added theorem UniformOnFun.ofFun_inv
added theorem UniformOnFun.ofFun_mul
modified theorem UniformOnFun.one_apply
added theorem UniformOnFun.toFun_div
added theorem UniformOnFun.toFun_inv
added theorem UniformOnFun.toFun_mul
added theorem UniformOnFun.toFun_one
modified def UniformFun.ofFun
added theorem UniformFun.ofFun_toFun
modified def UniformFun.toFun
added theorem UniformFun.toFun_ofFun
modified def UniformOnFun.ofFun
modified def UniformOnFun.toFun