basic): rename `cospherical_subset` (#16947)

Commit

3 years ago

refactor(geometry/euclidean/basic): rename `cospherical_subset` (#16947) Rename `cospherical_subset` to `cospherical.subset` to allow use of dot notation.

Author

jsm28

Parents

a08db7e9

mathlib 1e9b3df5 - refactor(geometry/euclidean/basic): rename `cospherical_subset` (#16947)

mathlib
1e9b3df5 - refactor(geometry/euclidean/basic): rename `cospherical_subset` (#16947)