Restriction of a closed compact set in a product space to a set of coordinates

We show that the image of a compact closed set s in a product Π i : ι, α i by the restriction to a subset of coordinates S : Set ι is a closed set.

The idea of the proof is to use isClosedMap_snd_of_compactSpace, which is the fact that if X is a compact topological space, then Prod.snd : X × Y → Y is a closed map.

We remark that s is included in the set Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s), and we build a homeomorphism Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s) ≃ₜ Sᶜ.restrict '' s × Π i : S, α i. Sᶜ.restrict '' s is a compact space since s is compact, and the lemma applies, with X = Sᶜ.restrict '' s and Y = Π i : S, α i.

noncomputable def Topology.reorderRestrictProd {ι : Type u_1} {α : ι → Type u_2} (S : Set ι) (s : Set ((j : ι) → α j)) (p : ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)) (j : ι) : α j

Given a set in a product space s : Set (Π j, α j) and a set of coordinates S : Set ι, Sᶜ.restrict '' s × (Π i : S, α i) is the set of functions that coincide with an element of s on Sᶜ and are arbitrary on S. reorderRestrictProd sends a term of that type to Π j, α j by looking for the value at j in one part of the product or the other depending on whether j is in S or not.

Equations

• Topology.reorderRestrictProd S s p j = if h : j ∈ S then p.2 ⟨j, h⟩ else ↑p.1 ⟨j, h⟩

@[simp]

theorem Topology.reorderRestrictProd_of_mem {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} (p : ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)) (j : ↑S) : reorderRestrictProd S s p ↑j = p.2 j

@[simp]

theorem Topology.reorderRestrictProd_of_compl {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} (p : ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)) (j : ↑Sᶜ) : reorderRestrictProd S s p ↑j = ↑p.1 j

@[simp]

theorem Topology.restrict_compl_reorderRestrictProd {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} (p : ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)) : Sᶜ.restrict (reorderRestrictProd S s p) = ↑p.1

theorem Topology.continuous_reorderRestrictProd {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [(i : ι) → TopologicalSpace (α i)] : Continuous (reorderRestrictProd S s)

theorem Topology.reorderRestrictProd_mem_preimage_image_restrict {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} (p : ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)) : reorderRestrictProd S s p ∈ Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s)

@[simp]

theorem Topology.reorderRestrictProd_restrict_compl {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} (x : ↑(Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s))) : reorderRestrictProd S s (⟨Sᶜ.restrict ↑x, ⋯⟩, fun (i : ↑S) => ↑x ↑i) = ↑x

noncomputable def Homeomorph.preimageImageRestrict {ι : Type u_1} (α : ι → Type u_3) [(i : ι) → TopologicalSpace (α i)] (S : Set ι) (s : Set ((j : ι) → α j)) : ↑(Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s)) ≃ₜ ↑(Sᶜ.restrict '' s) × ((i : ↑S) → α ↑i)

Homeomorphism between the set of functions that concide with a given set of functions away from a given set S, and dependent functions away from S times any value on S.

Equations

• One or more equations did not get rendered due to their size.

theorem Topology.image_snd_preimageImageRestrict {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [(i : ι) → TopologicalSpace (α i)] : Prod.snd '' (⇑(Homeomorph.preimageImageRestrict α S s) '' ((fun (x : ↑(Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s))) => ↑x) ⁻¹' s)) = S.restrict '' s

The image by preimageImageRestrict α S s of s seen as a set of Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s) is a set of Sᶜ.restrict '' s × (Π i : S, α i), and the image of that set by Prod.snd is S.restrict '' s.

Used in IsCompact.isClosed_image_restrict to prove that the restriction of a compact closed set in a product space to a set of coordinates is closed.

theorem IsCompact.isClosed_image_restrict {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [(i : ι) → TopologicalSpace (α i)] (S : Set ι) (hs_compact : IsCompact s) (hs_closed : IsClosed s) : IsClosed (S.restrict '' s)

The restriction of a compact closed set in a product space to a set of coordinates is closed.

theorem isClosedMap_restrict_of_compactSpace {ι : Type u_1} {α : ι → Type u_2} {S : Set ι} [(i : ι) → TopologicalSpace (α i)] [∀ (i : ι), CompactSpace (α i)] : IsClosedMap S.restrict

theorem IsClosed.isClosed_image_eval {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [(i : ι) → TopologicalSpace (α i)] (i : ι) (hs_compact : IsCompact s) (hs_closed : IsClosed s) : IsClosed ((fun (x : (i : ι) → α i) => x i) '' s)