mathlib

d3de289a - feat(topology/local_homeomorph): open_embedding.continuous_at_iff (#3599)

feat(topology/local_homeomorph): open_embedding.continuous_at_iff (#3599) ``` lemma continuous_at_iff {f : α → β} {g : β → γ} (hf : open_embedding f) {x : α} : continuous_at (g ∘ f) x ↔ continuous_at g (f x) := ``` Co-authored-by: Scott Morrison <scott.morrison@gmail.com>