Theorems · Theorem · general topology

continuousWithinAt_const_vadd_iff

∀ {α : Type u_2} {β : Type u_3} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G]
  [inst_2 : AddAction G α] [ContinuousConstVAdd G α] [inst_4 : TopologicalSpace β] {f : β → α} {b : β} {s : Set β}
  (c : G), ContinuousWithinAt (fun x => c +ᵥ f x) s b ↔ ContinuousWithinAt f s b

Defined in

Mathlib.Topology.Algebra.ConstMulAction

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupAddActionContinuousConstVAddTopologicalSpace