Documentation

Mathlib.Topology.IsClosedRestrict

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
Instances For
    @[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)) :
    theorem Topology.continuous_reorderRestrictProd {ι : Type u_1} {α : ιType u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [(i : ι) → TopologicalSpace (α i)] :
    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)) :
    @[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.
    Instances For
      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) :

      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)] :
      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)