English
If g: α → γ is continuous and has compact support, then g defines a bounded continuous function; in particular, there exists C with ∀ x, ∥g(x)∥ ≤ C.
Русский
Если g: α → γ непрерывна и имеет компактную опору, то она задаёт ограниченную непрерывную функцию; существует C, такое что ∀ x, ∥g(x)∥ ≤ C.
LaTeX
$$$\\exists C \\in \\mathbb{R},\\; \\forall x \\in \\alpha,\\; \\|g(x)\\| \\le C$$$
Lean4
/-- A compactly supported continuous function is automatically bounded. This constructor gives
an object of `α →ᵇ γ` from `g : α → γ` and these assumptions. -/
def ofCompactSupport (g : α → γ) (hg₁ : Continuous g) (hg₂ : HasCompactSupport g) : α →ᵇ γ
where
toFun := g
continuous_toFun := hg₁
map_bounded' := by
obtain (hs | hs) := (tsupport g).eq_empty_or_nonempty
· exact ⟨0, by simp [tsupport_eq_empty_iff.mp hs]⟩
· obtain ⟨z, _, hmax⟩ := hg₂.exists_isMaxOn hs <| hg₁.norm.continuousOn
refine ⟨2 * ‖g z‖, dist_le_two_norm' fun x ↦ ?_⟩
by_cases hx : x ∈ tsupport g
· exact isMaxOn_iff.mp hmax x hx
· simp [image_eq_zero_of_notMem_tsupport hx]
