Commit 2023-06-06 22:59 e0ca1161

View on Github →

style: rename Rtendsto and Ptendsto to RTendsto and PTendsto (#4722) https://github.com/leanprover-community/mathlib4/issues/2203

Estimated changes

added def Filter.PTendsto'
added def Filter.PTendsto
deleted def Filter.Ptendsto'
deleted def Filter.Ptendsto
added def Filter.RTendsto'
added def Filter.RTendsto
deleted def Filter.Rtendsto'
deleted def Filter.Rtendsto