English
If U is open in α' and f: U → β is continuous with HasCompactMulSupport, then the extension of f by 1 is continuous on U extended by 1.
Русский
Если U открыто в α' и f: U → β непрерывна с компактной мультиподдержкой, то продолжение f до единицы по U непрерывно на новом пространстве.
LaTeX
$$$\\text{IsOpen}(U) \\Rightarrow \\forall f: U\\to \\beta, \\ \\text{Continuous}(f) \\land \\text{HasCompactMulSupport}(f) \\Rightarrow \\text{Continuous}(\\text{Subtype.val.extend } f\\,1).$$$
Lean4
@[to_additive]
theorem continuous_extend_one [TopologicalSpace β] {U : Set α'} (hU : IsOpen U) {f : U → β} (cont : Continuous f)
(supp : HasCompactMulSupport f) : Continuous (Subtype.val.extend f 1) :=
continuous_of_mulTSupport fun x h ↦
by
rw [show x = ↑(⟨x, Subtype.coe_image_subset _ _ (supp.mulTSupport_extend_one_subset continuous_subtype_val h)⟩ : U)
by rfl,
← (hU.isOpenEmbedding_subtypeVal).continuousAt_iff, extend_comp Subtype.val_injective]
exact cont.continuousAt
