English
The disjoint sum of delta-generated spaces is delta-generated.
Русский
Дисъюнктное объединение дельта-генерируемых пространств является дельта-генерируемым.
LaTeX
$$$ \\DeltaGeneratedSpace(X \\oplus Y) $$$
Lean4
/-- The product of a compact space and a paracompact space is a paracompact space. The formalization
is based on https://dantopology.wordpress.com/2009/10/24/compact-x-paracompact-is-paracompact/
with some minor modifications.
This version assumes that `X` in `X × Y` is compact and `Y` is paracompact, see next lemma for the
other case. -/
instance (priority := 200) [CompactSpace X] [ParacompactSpace Y] : ParacompactSpace (X × Y) where
locallyFinite_refinement α s ho
hu :=
by
have : ∀ (x : X) (y : Y), ∃ (a : α) (U : Set X) (V : Set Y), IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ U ×ˢ V ⊆ s a :=
fun x y ↦ (iUnion_eq_univ_iff.1 hu (x, y)).imp fun a ha ↦ isOpen_prod_iff.1 (ho a) x y ha
choose a U V hUo hVo hxU hyV hUV using this
choose T hT using fun y ↦ CompactSpace.elim_nhds_subcover (U · y) fun x ↦ (hUo x y).mem_nhds (hxU x y)
set W : Y → Set Y := fun y ↦ ⋂ x ∈ T y, V x y
have hWo : ∀ y, IsOpen (W y) := fun y ↦ isOpen_biInter_finset fun _ _ ↦ hVo _ _
have hW : ∀ y, y ∈ W y := fun _ ↦ mem_iInter₂.2 fun _ _ ↦ hyV _ _
rcases precise_refinement W hWo (iUnion_eq_univ_iff.2 fun y ↦ ⟨y, hW y⟩) with ⟨E, hEo, hE, hEf, hEA⟩
refine
⟨Σ y, T y, fun z ↦ U z.2.1 z.1 ×ˢ E z.1, fun _ ↦ (hUo _ _).prod (hEo _), iUnion_eq_univ_iff.2 fun (x, y) ↦ ?_,
fun (x, y) ↦ ?_, fun ⟨y, x, hx⟩ ↦ ?_⟩
· rcases iUnion_eq_univ_iff.1 hE y with ⟨b, hb⟩
rcases iUnion₂_eq_univ_iff.1 (hT b) x with ⟨a, ha, hx⟩
exact ⟨⟨b, a, ha⟩, hx, hb⟩
· rcases hEf y with ⟨t, ht, htf⟩
refine ⟨univ ×ˢ t, prod_mem_nhds univ_mem ht, ?_⟩
refine (htf.biUnion fun y _ ↦ finite_range (Sigma.mk y)).subset ?_
rintro ⟨b, a, ha⟩ ⟨⟨c, d⟩, ⟨-, hd : d ∈ E b⟩, -, hdt : d ∈ t⟩
exact mem_iUnion₂.2 ⟨b, ⟨d, hd, hdt⟩, mem_range_self _⟩
· refine ⟨a x y, (Set.prod_mono Subset.rfl ?_).trans (hUV x y)⟩
exact (hEA _).trans (iInter₂_subset x hx)
