Theorems · Theorem · general topology

ContinuousAt.div_const

∀ {α : Type u_1} {G₀ : Type u_3} [inst : DivInvMonoid G₀] [inst_1 : TopologicalSpace G₀] [SeparatelyContinuousMul G₀]
  {f : α → G₀} [inst_3 : TopologicalSpace α] {a : α}, ContinuousAt f a → ∀ (y : G₀), ContinuousAt (fun x => f x / y) a

Defined in

Mathlib.Topology.Algebra.GroupWithZero

Cited by

2 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Quot.sound

Assumes

DivInvMonoidTopologicalSpaceSeparatelyContinuousMulTopologicalSpace