Commit 2020-09-29 03:32 88187ba9

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.