English
A set is locally constructible if at every point there exists a neighborhood where the set is constructible.
Русский
Множество локально конструируемое, если вокруг каждой точки есть окрестность, где множество конструктивно.
LaTeX
$$$IsLocallyConstructible(s) = \\forall x, \\exists U \\in 𝓝(x), IsOpen(U) \\land IsConstructible(U \\cap s).$$$
Lean4
@[elab_as_elim]
theorem induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι] (b : ι → Set X) (basis : IsTopologicalBasis (range b))
(isCompact_basis : ∀ i, IsCompact (b i))
(sdiff :
∀ i s (hs : Set.Finite s),
P (b i \ ⋃ j ∈ s, b j)
(((isCompact_basis _).isConstructible (basis.isOpen ⟨i, rfl⟩)).sdiff <|
.biUnion hs fun _ _ ↦ ((isCompact_basis _).isConstructible (basis.isOpen ⟨_, rfl⟩))))
(union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht)) (s : Set X) (hs : IsConstructible s) : P s hs := by
induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with
| isSublattice =>
exact
⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩, fun s hs t ht ↦
⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩
| bot_mem => exact ⟨isOpen_empty, .empty⟩
| top_mem => exact ⟨isOpen_univ, .univ⟩
| sdiff U hU V
hV =>
have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis isCompact_basis
obtain ⟨s, hs, rfl⟩ := (this _).1 ⟨hU.2.isCompact, hU.1⟩
obtain ⟨t, ht, rfl⟩ := (this _).1 ⟨hV.2.isCompact, hV.1⟩
simp_rw [iUnion_diff]
induction s, hs using Set.Finite.induction_on with
| empty => simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _}
| @insert i s hi hs ih =>
simp_rw [biUnion_insert]
exact
union _ _ _
(.biUnion hs fun i _ ↦
((isCompact_basis _).isConstructible (basis.isOpen ⟨i, rfl⟩)).sdiff <|
.biUnion ht fun j _ ↦ (isCompact_basis _).isConstructible (basis.isOpen ⟨_, rfl⟩))
(sdiff _ _ ht)
(ih
⟨isOpen_biUnion fun _ _ ↦ basis.isOpen ⟨_, rfl⟩,
.biUnion hs fun i _ ↦ (isCompact_basis _).isRetrocompact (basis.isOpen ⟨i, rfl⟩)⟩)
| sup s _ t _ hs' ht' => exact union _ _ _ _ hs' ht'
