Results about projections

theorem continuous_cast {α : Type u} {β : Type u} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (h : α = β) (ht : HEq tα tβ) : Continuous fun (x : α) => cast h x

theorem measurable_proj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (I : Set ι) : Measurable fun (f : (i : ι) → α i) (i : ↑I) => f ↑i

theorem measurable_proj' {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (I : Finset ι) : Measurable fun (f : (i : ι) → α i) (i : { x : ι // x ∈ I }) => f ↑i

theorem measurable_proj₂ {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (I : Set ι) (J : Set ι) (hIJ : J ⊆ I) : Measurable fun (f : (i : ↑I) → α ↑i) (i : ↑J) => f ⟨↑i, ⋯⟩

theorem measurable_proj₂' {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (I : Finset ι) (J : Finset ι) (hIJ : J ⊆ I) : Measurable fun (f : (i : { x : ι // x ∈ I }) → α ↑i) (i : { x : ι // x ∈ J }) => f ⟨↑i, ⋯⟩

theorem continuous_proj {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] (I : Set ι) : Continuous fun (f : (i : ι) → α i) (i : ↑I) => f ↑i

theorem continuous_proj₂ {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] (I : Set ι) (J : Set ι) (hIJ : J ⊆ I) : Continuous fun (f : (i : ↑I) → α ↑i) (i : ↑J) => f ⟨↑i, ⋯⟩

theorem continuous_proj₂' {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] (I : Finset ι) (J : Finset ι) (hIJ : J ⊆ I) : Continuous fun (f : (i : { x : ι // x ∈ I }) → α ↑i) (i : { x : ι // x ∈ J }) => f ⟨↑i, ⋯⟩

We show that the projection of a compact closed set s in a product Π i, α i onto one of the spaces α j 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. In our application, Y is α j and X is the projection of s to the product over all indexes that are not j. We define projCompl α j for that projection map.

In order to be able to use the lemma isClosedMap_snd_of_compactSpace, we have to make those X and Y appear explicitly. We remark that s belongs to the set projCompl α j ⁻¹' (projCompl α j '' s), and we build an homeomorphism projCompl α j ⁻¹' (projCompl α j '' s) ≃ₜ projCompl α j '' s × α j. projCompl α j is a compact space since s is compact, and the lemma applies.

def projCompl {ι : Type u_3} (α : ι → Type u_5) (i : ι) (x : (i : ι) → α i) (j : { k : ι // k ≠ i }) : α ↑j

Given a dependent function of i, specialize it as a function on the complement of {i}.

Equations

• projCompl α i x j = x ↑j

theorem continuous_projCompl {ι : Type u_3} {α : ι → Type u_4} {i : ι} [(i : ι) → TopologicalSpace (α i)] : Continuous (projCompl α i)

noncomputable def fromXProd {ι : Type u_3} (α : ι → Type u_5) (i : ι) (s : Set ((j : ι) → α j)) (p : ↑(projCompl α i '' s) × α i) (j : ι) : α j

Given a set of dependent functions, construct a function on a product space separating out the coordinate i from the other ones.

Equations

• fromXProd α i s p j = if h : j = i then cast ⋯ p.2 else ↑p.1 ⟨j, h⟩

@[simp]

theorem fromXProd_same {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} (p : ↑(projCompl α i '' s) × α i) : fromXProd α i s p i = p.2

@[simp]

theorem projCompl_fromXProd {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} (p : ↑(projCompl α i '' s) × α i) : projCompl α i (fromXProd α i s p) = ↑p.1

theorem continuous_fromXProd {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} [(i : ι) → TopologicalSpace (α i)] : Continuous (fromXProd α i s)

theorem fromXProd_mem_XY {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} (p : ↑(projCompl α i '' s) × α i) : fromXProd α i s p ∈ projCompl α i ⁻¹' (projCompl α i '' s)

@[simp]

theorem fromXProd_projCompl {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} (x : ↑(projCompl α i ⁻¹' (projCompl α i '' s))) : fromXProd α i s (⟨projCompl α i ↑x, ⋯⟩, ↑x i) = ↑x

noncomputable def XYEquiv {ι : Type u_3} (α : ι → Type u_5) [(i : ι) → TopologicalSpace (α i)] (i : ι) (s : Set ((j : ι) → α j)) : ↑(projCompl α i ⁻¹' (projCompl α i '' s)) ≃ₜ ↑(projCompl α i '' s) × α i

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

Equations

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

theorem preimage_snd_xyEquiv {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} {i : ι} [(i : ι) → TopologicalSpace (α i)] : Prod.snd '' (⇑(XYEquiv α i s) '' ((fun (x : ↑(projCompl α i ⁻¹' (projCompl α i '' s))) => ↑x) ⁻¹' s)) = (fun (x : (i : ι) → α i) => x i) '' s

theorem isClosed_proj {ι : Type u_3} {α : ι → Type u_4} {s : Set ((i : ι) → α i)} [(i : ι) → TopologicalSpace (α i)] (hs_compact : IsCompact s) (hs_closed : IsClosed s) (i : ι) : IsClosed ((fun (x : (i : ι) → α i) => x i) '' s)

The projection of a compact closed set onto a coordinate is closed.