English
In a paracompact space, every open cover has a locally finite precise refinement indexed by the same type, where each refined set sits inside the corresponding original set.
Русский
В паракомпактном пространстве любое открытое покрытие имеет локально конечное точное разбиение, индексируемое тем же типом, причём каждая новая секция находится внутри соответствующей исходной секции.
LaTeX
$$$ \\exists v : ι \\to Set X, \\left( \\forall a, IsOpen(v(a)) \\right) \\land \\left( \\bigcup_i v(i) = univ \\right) \\land LocallyFinite v \\land \\forall a, v(a) \\subseteq u(a). $$$
Lean4
/-- Any open cover of a paracompact space has a locally finite *precise* refinement, that is,
one indexed on the same type with each open set contained in the corresponding original one. -/
theorem precise_refinement [ParacompactSpace X] (u : ι → Set X) (uo : ∀ a, IsOpen (u a)) (uc : ⋃ i, u i = univ) :
∃ v : ι → Set X, (∀ a, IsOpen (v a)) ∧ ⋃ i, v i = univ ∧ LocallyFinite v ∧ ∀ a, v a ⊆ u a := by
-- Apply definition to `range u`, then turn existence quantifiers into functions using `choose`
have :=
ParacompactSpace.locallyFinite_refinement (range u) (fun r ↦ (r : Set X)) (forall_subtype_range_iff.2 uo)
(by rwa [← sUnion_range, Subtype.range_coe])
simp only [exists_subtype_range_iff, iUnion_eq_univ_iff] at this
choose α t hto hXt htf ind hind using this
choose t_inv ht_inv using hXt
choose U hxU hU using htf
refine ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, ?_, ?_, ?_, ?_⟩
· exact fun a ↦ isOpen_iUnion fun a ↦ isOpen_iUnion fun _ ↦ hto a
· simp only [eq_univ_iff_forall, mem_iUnion]
exact fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩
· refine fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset ?_⟩
simp only [subset_def, mem_iUnion, mem_setOf_eq, Set.Nonempty, mem_inter_iff]
rintro i ⟨y, ⟨a, rfl, hya⟩, hyU⟩
exact mem_image_of_mem _ ⟨y, hya, hyU⟩
· simp only [subset_def, mem_iUnion]
rintro i x ⟨a, rfl, hxa⟩
exact hind _ hxa
