proposition: Lemma continuity_2d_pt_neq_0 : forall f x y, continuity_2d_pt f x y -> f x y <> 0 -> locally_2d (fun u v => f u v <> 0) x y.
proof: Proof. intros f x y Cf H. apply continuity_2d_pt_filterlim in Cf. apply locally_2d_locally. apply (Cf (fun y => y <> 0)). now apply open_neq. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq