[Merged by Bors] - chore: deprecate Analysis/Normed/Order/Basic#34047

grunweg wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:normedorderbasicgrunweg/mathlib4:normedorderbasicCopy head branch name to clipboard