English
The image under the second projection of the restricted preimage image map equals the restricted image of s.
Русский
Изображение по второй проекции от ограниченного предобраза равно ограниченному образу s.
LaTeX
$$$\\operatorname{Prod}.\\operatorname{snd} '' (\\operatorname{preimageImageRestrict}(\\alpha,S,s) '' (\\dots)) = S^{\\text{re}}'' s.$$$
Lean4
/-- 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 image_snd_preimageImageRestrict [∀ i, TopologicalSpace (α i)] :
Prod.snd ''
(Homeomorph.preimageImageRestrict α S s ''
((fun (x : Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s)) ↦ (x : Π j, α j)) ⁻¹' s)) =
S.restrict '' s :=
by
ext x
simp only [Homeomorph.preimageImageRestrict, Homeomorph.homeomorph_mk_coe, Equiv.coe_fn_mk, mem_image, mem_preimage,
Subtype.exists, exists_and_left, Prod.exists, Prod.mk.injEq, exists_and_right, exists_eq_right, Subtype.mk.injEq,
exists_prop]
constructor
· rintro ⟨y, _, z, hz_mem, _, hzx⟩
exact ⟨z, hz_mem, hzx⟩
· rintro ⟨z, hz_mem, hzx⟩
exact ⟨Sᶜ.restrict z, mem_image_of_mem Sᶜ.restrict hz_mem, z, hz_mem, ⟨⟨⟨z, hz_mem, rfl⟩, rfl⟩, hzx⟩⟩
