English
If s and t are locally constructible, their union is locally constructible.
Русский
Если s и t локально конструируемы, их объединение конструируемо локально.
LaTeX
$$$IsLocallyConstructible(s) \\land IsLocallyConstructible(t) \\Rightarrow IsLocallyConstructible(s \\cup t).$$$
Lean4
theorem union (hs : IsLocallyConstructible s) (ht : IsLocallyConstructible t) : IsLocallyConstructible (s ∪ t) :=
by
rintro x
obtain ⟨U, hxU, hU, hsU⟩ := hs x
obtain ⟨V, hxV, hV, htV⟩ := ht x
refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩
have : (U ∩ V) ↓∩ (s ∪ t) = inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∪ inclusion inter_subset_right ⁻¹' (V ↓∩ t) := by
ext; simp
rw [this]
exact
.union (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <| .preimage continuous_subtype_val <| hU.inter hV)
(htV.preimage_of_isOpenEmbedding <| .inclusion _ <| .preimage continuous_subtype_val <| hU.inter hV)
