Theorems · Theorem · general topology

ContinuousAt.comp_div_cases

∀ {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
  [ContinuousInv₀ G₀] [ContinuousMul G₀] [inst_4 : TopologicalSpace α] [inst_5 : TopologicalSpace β] {a : α}
  {f g : α → G₀} (h : α → G₀ → β),
  ContinuousAt f a →
    ContinuousAt g a →
      (g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)) →
        (g a = 0 → Filter.Tendsto (↿h) (nhds a ×ˢ ⊤) (nhds (h a 0))) → ContinuousAt (fun x => h x (f x / g x)) a

The function f x / g x is discontinuous when g x = 0. However, under appropriate conditions, h x (f x / g x) is still continuous. The condition is that if g a = 0 then h x y must tend to h a 0 when x tends to a, with no information about y. This is represented by the ⊤ filter. Note: tendsto_prod_top_iff characterizes this convergence in uniform spaces. See also Filter.prod_top and Filter.mem_prod_top.

Defined in

Mathlib.Topology.Algebra.GroupWithZero

Cited by

1 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupWithZeroTopologicalSpaceContinuousInv₀ContinuousMulTopologicalSpaceTopologicalSpace