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
.
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⟩
Instances For
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.
Instances For
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.
The restriction of a compact closed set in a product space to a set of coordinates is closed.