chore(topology/algebra/ordered): golf a proof (#4311)
* generalize `continuous_within_at_Ioi_iff_Ici` from `linear_order α`
to `partial_order α`;
* base the proof on a more general fact:
`continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x`.
