English
In a locally compact Hausdorff space, given a partial refinement v and a compact closure assumption, one can strictly enlarge v at a new index i while preserving compactness of the new closure.
Русский
В локально компактном расслоенном пространстве Х: при наличии частичного уточнения v и допуска компактности замыкающей части, можно строго увеличить v по новому индексу i, сохранив компактность замыкания нового множества.
LaTeX
$$$$\exists v' : PartialRefinement u s (fun w => IsCompact (closure w)), v < v' \land IsCompact (closure (v' i)).$$$$
Lean4
/-- In a locally compact Hausdorff space `X`, if `s` is a compact set, `v` is a partial refinement,
and `i` is an index such that `i ∉ v.carrier`, then there exists a partial refinement that is
strictly greater than `v`. -/
theorem exists_gt_t2space (v : PartialRefinement u s (fun w => IsCompact (closure w))) (hs : IsCompact s) (i : ι)
(hi : i ∉ v.carrier) :
∃ v' : PartialRefinement u s (fun w => IsCompact (closure w)), v < v' ∧ IsCompact (closure (v' i)) := by
-- take `v i` such that `closure (v i)` is compact
set si := s ∩ (⋃ j ≠ i, v j)ᶜ with hsi
simp only [ne_eq, compl_iUnion] at hsi
have hsic : IsCompact si := by
apply IsCompact.of_isClosed_subset hs _ Set.inter_subset_left
· have : IsOpen (⋃ j ≠ i, v j) := by
apply isOpen_biUnion
intro j _
exact v.isOpen j
exact IsClosed.inter (IsCompact.isClosed hs) (IsOpen.isClosed_compl this)
have : si ⊆ v i := by
intro x hx
have (j) (hj : j ≠ i) : x ∉ v j := by
rw [hsi] at hx
apply Set.notMem_of_mem_compl
have hsi' : x ∈ (⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ) := Set.mem_of_mem_inter_right hx
rw [ne_eq] at hj
rw [Set.mem_iInter₂] at hsi'
exact hsi' j hj
obtain ⟨j, hj⟩ := Set.mem_iUnion.mp (v.subset_iUnion (Set.mem_of_mem_inter_left hx))
obtain rfl : j = i := by
by_contra! h
exact this j h hj
exact hj
obtain ⟨vi, hvi⟩ := exists_open_between_and_isCompact_closure hsic (v.isOpen i) this
classical
refine ⟨⟨update v i vi, insert i v.carrier, ?_, ?_, ?_, ?_, ?_⟩, ⟨?_, ?_⟩, ?_⟩
· intro j
rcases eq_or_ne j i with (rfl | hne) <;> simp [*, v.isOpen]
· refine fun x hx => mem_iUnion.2 ?_
rcases em (∃ j ≠ i, x ∈ v j) with (⟨j, hji, hj⟩ | h)
· use j
rwa [update_of_ne hji]
· push_neg at h
use i
rw [update_self]
apply hvi.2.1
rw [hsi]
exact ⟨hx, mem_iInter₂_of_mem h⟩
· rintro j (rfl | hj)
· rw [update_self]
exact subset_trans hvi.2.2.1 <| PartialRefinement.subset v j
· rw [update_of_ne (ne_of_mem_of_not_mem hj hi)]
exact v.closure_subset hj
· intro j hj
rw [mem_insert_iff] at hj
by_cases h : j = i
· rw [← h]
simp only [update_self]
exact hvi.2.2.2
· apply hj.elim
· intro hji
exact False.elim (h hji)
· intro hjmemv
rw [update_of_ne h]
exact v.pred_of_mem hjmemv
· intro j hj
rw [mem_insert_iff, not_or] at hj
rw [update_of_ne hj.1, v.apply_eq hj.2]
· refine ⟨subset_insert _ _, fun j hj => ?_⟩
exact (update_of_ne (ne_of_mem_of_not_mem hj hi) _ _).symm
· exact fun hle => hi (hle.1 <| mem_insert _ _)
· simp only [update_self]
exact hvi.2.2.2
