English
Induction on a topological basis yields that any constructible set can be built from basis elements by unions and set differences.
Русский
Индукция по базису топологий показывает, что конструируемое множество строится из элементов базиса с помощью объединений и разностей.
LaTeX
$$$\\text{induction\_of\_isTopologicalBasis}(\dots) \\Rightarrow \\text{IsConstructible}(s) \\Rightarrow \\dots$$$
Lean4
theorem inter (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, ?_⟩
change IsConstructible (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t))
exact
.inter (hsU.preimage_of_isOpenEmbedding <| .inclusion _ <| .preimage continuous_subtype_val <| hU.inter hV)
(htV.preimage_of_isOpenEmbedding <| .inclusion _ <| .preimage continuous_subtype_val <| hU.inter hV)
