Topological support of a translate

The topological support of a right translate of a function on a topological group, and of a function transported along a homeomorphism, next to Mathlib's mulTSupport_comp_eq_preimage.

Main results

• TauCeti.mulTSupport_comp_div_right: the topological multiplicative support of fun y => f (y / x) is the preimage of that of f under (· / x), with additive version TauCeti.tsupport_comp_sub_right.
• Homeomorph.tsupport_comp_symm: transporting a function F along a homeomorphism e gives F ∘ e⁻¹, whose topological support is e(tsupport F), with multiplicative version Homeomorph.mulTSupport_comp_symm.
• Homeomorph.tsupport_comp_symm_subset_interior_image: support in the interior of a set is transported to support in the interior of its image, with multiplicative version Homeomorph.mulTSupport_comp_symm_subset_interior_image.
• Continuous.smul_of_continuousOn_of_tsupport_subset: a continuous function supported in U, times a function continuous on U, is continuous.
• TauCeti.tsupport_snd_smul_fst_subset: the topological support of (x, y) ↦ f y • g x lies in tsupport g ×ˢ tsupport f.

theorem TauCeti.mulTSupport_comp_div_right {X : Type u_1} {G : Type u_2} [TopologicalSpace X] [Group X] [SeparatelyContinuousMul X] [One G] (f : X → G) (x : X) : (mulTSupport fun (y : X) => f (y / x)) = (fun (x_1 : X) => x_1 / x) ⁻¹' mulTSupport f

The topological multiplicative support of a right translate is the preimage of the topological multiplicative support under the opposite translation.

theorem TauCeti.tsupport_comp_sub_right {X : Type u_1} {G : Type u_2} [TopologicalSpace X] [AddGroup X] [SeparatelyContinuousAdd X] [Zero G] (f : X → G) (x : X) : (tsupport fun (y : X) => f (y - x)) = (fun (x_1 : X) => x_1 - x) ⁻¹' tsupport f

The topological support of a translate is the translated topological support.

theorem TauCeti.support_snd_smul_fst_subset {X : Type u_1} {Y : Type u_3} {R : Type u_4} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] (f : Y → R) (g : X → M) : (Function.support fun (p : X × Y) => f p.2 • g p.1) ⊆ Function.support g ×ˢ Function.support f

The function (x, y) ↦ f y • g x is supported in support g ×ˢ support f.

theorem TauCeti.tsupport_snd_smul_fst_subset {X : Type u_1} [TopologicalSpace X] {Y : Type u_3} {R : Type u_4} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [TopologicalSpace Y] (f : Y → R) (g : X → M) : (tsupport fun (p : X × Y) => f p.2 • g p.1) ⊆ tsupport g ×ˢ tsupport f

The function (x, y) ↦ f y • g x is supported in tsupport g ×ˢ tsupport f.

theorem Continuous.smul_of_continuousOn_of_tsupport_subset {Z : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [TopologicalSpace Z] [TopologicalSpace 𝕜] [Zero F] [TopologicalSpace F] [SMulZeroClass 𝕜 F] [ContinuousSMul 𝕜 F] {a : Z → 𝕜} {b : Z → F} {U : Set Z} (hb : Continuous b) (hbU : tsupport b ⊆ U) (ha : ContinuousOn a U) : Continuous fun (x : Z) => a x • b x

A function b continuous with topological support in U, times a function a continuous on U, is continuous. The function a need not be continuous off U, and U need not be open.

theorem Homeomorph.mulTSupport_comp_symm {X : Type u_1} {Y : Type u_2} {α : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [One α] (e : X ≃ₜ Y) (F : X → α) : mulTSupport (F ∘ ⇑e.symm) = ⇑e '' mulTSupport F

The topological multiplicative support of a function transported along a homeomorphism e is the image under e of its topological multiplicative support.

theorem Homeomorph.tsupport_comp_symm {X : Type u_1} {Y : Type u_2} {α : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Zero α] (e : X ≃ₜ Y) (F : X → α) : tsupport (F ∘ ⇑e.symm) = ⇑e '' tsupport F

The topological support of a function transported along a homeomorphism e is the image under e of its topological support.

theorem Homeomorph.mulTSupport_comp_symm_subset_interior_image {X : Type u_1} {Y : Type u_2} {α : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [One α] (e : X ≃ₜ Y) {F : X → α} {s : Set X} (h : mulTSupport F ⊆ interior s) : mulTSupport (F ∘ ⇑e.symm) ⊆ interior (⇑e '' s)

A function whose topological multiplicative support lies in the interior of s, transported along a homeomorphism e, has topological multiplicative support in the interior of e(s).

theorem Homeomorph.tsupport_comp_symm_subset_interior_image {X : Type u_1} {Y : Type u_2} {α : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Zero α] (e : X ≃ₜ Y) {F : X → α} {s : Set X} (h : tsupport F ⊆ interior s) : tsupport (F ∘ ⇑e.symm) ⊆ interior (⇑e '' s)

A function supported in the interior of s, transported along a homeomorphism e, is supported in the interior of e(s).