Theorems · Theorem · functional analysis

AddMonoidHom.continuous_of_isBounded_nhds_zero

∀ {G : Type u_6} {H : Type u_7} [inst : SeminormedAddCommGroup G] [inst_1 : SeminormedAddCommGroup H] [NormedSpace ℝ H]
  {s : Set G} (f : G →+ H), s ∈ nhds 0 → Bornology.IsBounded (⇑f '' s) → Continuous ⇑f

A group homomorphism from a normed group to a real normed space, bounded on a neighborhood of 0, must be continuous.

Defined in

Mathlib.Analysis.Normed.Module.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNormedSpace