Commit 2023-06-02 11:44 bac5670d

View on Github →

chore: fix some names (#4564)

  • Protect HasFTaylorSeriesUpToOn.fderivWithin, IsBoundedBilinearMap.fderiv, and IsBoundedBilinearMap.fderivWithin.
  • Rename
    • isBoundedBilinearMapSmul -> isBoundedBilinearMap_smul;
    • isBoundedBilinearMapMul -> isBoundedBilinearMap_mul;
    • isBoundedBilinearMapComp -> isBoundedBilinearMap_comp;
    • isBoundedBilinearMapSmulRight -> isBoundedBilinearMap_smulRight;
    • isBoundedBilinearMapCompMultilinear -> isBoundedBilinearMap_compMultilinear;
    • ContinuousLinearMap.mulLeftRightIsBoundedBilinear -> ContinuousLinearMap.mulLeftRight_isBoundedBilinear;
    • nhdsWithin_eq_nhds_within' -> nhdsWithin_eq_nhdsWithin';
    • ContinuousWithinAt.preimage_mem_nhds_within' -> ContinuousWithinAt.preimage_mem_nhdsWithin'.

Estimated changes

deleted theorem isBoundedBilinearMapComp
deleted theorem isBoundedBilinearMapMul
deleted theorem isBoundedBilinearMapSmul