Theorems · Theorem · functional analysis

ContinuousWithinAt.nnnorm

∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {f : α → E} {s : Set α}
  {a : α}, ContinuousWithinAt f s a → ContinuousWithinAt (fun x => ‖f x‖₊) s a

Defined in

Mathlib.Analysis.Normed.Group.Continuity

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddGroupTopologicalSpace