Uniform local norm bounds over compact parameter spaces #
This file records a uniform local boundedness consequence of continuity over a compact family.
Main declarations #
TauCeti.exists_eventually_norm_le_compact_family: a continuous family indexed by a compact parameter space is uniformly bounded near any fiber contained in its open domain.
theorem
TauCeti.exists_eventually_norm_le_compact_family
{X : Type u_1}
{P : Type u_2}
{α : Type u_3}
{H : Type u_4}
[TopologicalSpace X]
[TopologicalSpace P]
[TopologicalSpace α]
[CompactSpace α]
[NormedAddCommGroup H]
{W : Set (X × P)}
{F : X × P → H}
{ι : α → P}
(hι : Continuous ι)
(hW : IsOpen W)
(hF : ContinuousOn F W)
{x₀ : X}
(hx₀ : ∀ (y : α), (x₀, ι y) ∈ W)
:
A function continuous on an open set W ⊆ X × P is bounded on {x} × ι(α), uniformly for
x near a point x₀ with {x₀} × ι(α) ⊆ W, when α is compact and ι is continuous.