English
There is a bounded continuous extension of a map defined on α to δ when δ has the discrete topology, given by the discrete extension construction.
Русский
Существуют дискретное расширение отображения из α в δ до δ, сохраняющее ограниченность и непрерывность.
LaTeX
$$$\\text{extend}(f,g,h) \\in \\delta \\to^\\mathrm{b} \\beta$$$
Lean4
/-- A version of `Function.extend` for bounded continuous maps. We assume that the domain has
discrete topology, so we only need to verify boundedness. -/
nonrec def extend (f : α ↪ δ) (g : α →ᵇ β) (h : δ →ᵇ β) : δ →ᵇ β
where
toFun := extend f g h
continuous_toFun := continuous_of_discreteTopology
map_bounded' := by
rw [← isBounded_range_iff, range_extend f.injective]
exact g.isBounded_range.union (h.isBounded_image _)
