English
If U is an open cover and each s ∩ U_i is locally constructible, then s is locally constructible.
Русский
Если U — открытое покрытие пространства, и каждый s ∩ U_i локально конструируем, то s локально конструируем.
LaTeX
$$$\\text{IsOpenCover}(U)\\ \\wedge\\ \\forall i, \\operatorname{IsLocallyConstructible}(s \\cap U_i) \\Rightarrow \\operatorname{IsLocallyConstructible}(s).$$$
Lean4
theorem of_isOpenCover (hU : IsOpenCover U) (H : ∀ i, IsLocallyConstructible ((U i : Set X) ↓∩ s)) :
IsLocallyConstructible s := by
intro x
have ⟨i, hi⟩ := hU.exists_mem x
have ⟨V, hVx, hV, hV'⟩ := H i ⟨x, hi⟩
refine ⟨_, (U i).2.isOpenEmbedding_subtypeVal.image_mem_nhds.mpr hVx, (U i).2.isOpenMap_subtype_val _ hV, ?_⟩
let e : V ≃ₜ Subtype.val '' V :=
(Equiv.Set.image _ V Subtype.val_injective).toHomeomorphOfIsInducing
((U i).2.isOpenEmbedding_subtypeVal.restrict (by simp [MapsTo]) hV).isInducing
convert hV'.preimage_of_isOpenEmbedding e.symm.isOpenEmbedding
ext ⟨_, x, hx, rfl⟩
simp [e, Equiv.toHomeomorphOfIsInducing]
