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 <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib