ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hu : (⋃ (a : α), s a) = univ
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hu : (⋃ (a : α), s a) = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
choose U hUo hU using fun a ↦ he.isOpen_iff.1 (ho a)
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
hu : (⋃ (a : α), s a) = univ
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
simp only [← hU] at hu ⊢
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
have heU : range e ⊆ ⋃ i, U i := by
  simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
rcases precise_refinement_set he.closed_range U hUo heU with ⟨V, hVo, heV, hVf, hVU⟩
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ (⋃ (b : α), (fun a => e ⁻¹' V a) b) = univ
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ ∃ β t h h, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ e ⁻¹' U a
refine ⟨α, fun a ↦ e ⁻¹' (V a), fun a ↦ (hVo a).preimage he.continuous, ?_,
  hVf.preimage_continuous he.continuous, fun a ↦ ⟨a, preimage_mono (hVU a)⟩⟩
no goals
case intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
heU : range e ⊆ ⋃ (i : α), U i
V : α → Set Y
hVo : ∀ (i : α), IsOpen (V i)
heV : range e ⊆ ⋃ (i : α), V i
hVf : LocallyFinite V
hVU : ∀ (i : α), V i ⊆ U i
⊢ (⋃ (b : α), (fun a => e ⁻¹' V a) b) = univ
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using heV
no goals
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace Y
e : X → Y
he : ClosedEmbedding e
α : Type v
s : α → Set X
ho : ∀ (a : α), IsOpen (s a)
U : α → Set Y
hUo : ∀ (a : α), IsOpen (U a)
hU : ∀ (a : α), e ⁻¹' U a = s a
hu : (⋃ (a : α), e ⁻¹' U a) = univ
⊢ range e ⊆ ⋃ (i : α), U i
simpa only [range_subset_iff, mem_iUnion, iUnion_eq_univ_iff] using hu