Theorems · Theorem · general topology

ContinuousOn.div_const

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

Defined in

Mathlib.Topology.Algebra.GroupWithZero

Cited by

3 results in Mathlib

Foundations

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

Assumes

DivInvMonoidTopologicalSpaceSeparatelyContinuousMulTopologicalSpace