ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
this : ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ (fun r => ↑r) a
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
have := ParacompactSpace.locallyFinite_refinement (range u) (fun r ↦ (r : Set X))
  (SetCoe.forall.2 <| forall_range_iff.2 uo) (by rwa [← sUnion_range, Subtype.range_coe])
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
this : ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ (∀ (x : X), ∃ i, x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ i, t b ⊆ u i
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
this : ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ (fun r => ↑r) a
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
simp only [SetCoe.exists, exists_range_iff', iUnion_eq_univ_iff, exists_prop] at this
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
hXt : ∀ (x : X), ∃ i, x ∈ t i
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
this : ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ (∀ (x : X), ∃ i, x ∈ t i) ∧ LocallyFinite t ∧ ∀ (b : β), ∃ i, t b ⊆ u i
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
choose α t hto hXt htf ind hind using this
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
hXt : ∀ (x : X), ∃ i, x ∈ t i
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
choose t_inv ht_inv using hXt
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
htf : LocallyFinite t
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
choose U hxU hU using htf
case refine'_1
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), IsOpen ((fun i => ⋃ (a : α) (_ : ind a = i), t a) a)

case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ (⋃ (i : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) i) = univ

case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ LocallyFinite fun i => ⋃ (a : α) (_ : ind a = i), t a

case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) a ⊆ u a
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ (⋃ (i : ι), v i) = univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
refine' ⟨fun i ↦ ⋃ (a : α) (_ : ind a = i), t a, _, _, _, _⟩
no goals
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
⊢ (⋃ (a : ↑(range u)), (fun r => ↑r) a) = univ
rwa [← sUnion_range, Subtype.range_coe]
no goals
case refine'_1
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), IsOpen ((fun i => ⋃ (a : α) (_ : ind a = i), t a) a)
exact fun a ↦ isOpen_iUnion fun a ↦ isOpen_iUnion fun _ ↦ hto a
case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (x : X), ∃ i i_1 i, x ∈ t i_1
case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ (⋃ (i : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) i) = univ
simp only [eq_univ_iff_forall, mem_iUnion]
no goals
case refine'_2
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (x : X), ∃ i i_1 i, x ∈ t i_1
exact fun x ↦ ⟨ind (t_inv x), _, rfl, ht_inv _⟩
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ {i | Set.Nonempty ((fun i => ⋃ (a : α) (_ : ind a = i), t a) i ∩ U x)} ⊆ ind '' {i | Set.Nonempty (t i ∩ U x)}
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ LocallyFinite fun i => ⋃ (a : α) (_ : ind a = i), t a
refine' fun x ↦ ⟨U x, hxU x, ((hU x).image ind).subset _⟩
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ ∀ (x_1 : ι), (∃ x_2, (∃ i i_1, x_2 ∈ t i) ∧ x_2 ∈ U x) → x_1 ∈ ind '' {i | ∃ x_2, x_2 ∈ t i ∧ x_2 ∈ U x}
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ {i | Set.Nonempty ((fun i => ⋃ (a : α) (_ : ind a = i), t a) i ∩ U x)} ⊆ ind '' {i | Set.Nonempty (t i ∩ U x)}
simp only [subset_def, mem_iUnion, mem_setOf_eq, Set.Nonempty, mem_inter_iff]
case refine'_3.intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i | ∃ x_1, x_1 ∈ t i ∧ x_1 ∈ U x}
case refine'_3
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
⊢ ∀ (x_1 : ι), (∃ x_2, (∃ i i_1, x_2 ∈ t i) ∧ x_2 ∈ U x) → x_1 ∈ ind '' {i | ∃ x_2, x_2 ∈ t i ∧ x_2 ∈ U x}
rintro i ⟨y, ⟨a, rfl, hya⟩, hyU⟩
no goals
case refine'_3.intro.intro.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i | ∃ x_1, x_1 ∈ t i ∧ x_1 ∈ U x}
exact mem_image_of_mem _ ⟨y, hya, hyU⟩
case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι) (x : X), (∃ i i_1, x ∈ t i) → x ∈ u a
case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι), (fun i => ⋃ (a : α) (_ : ind a = i), t a) a ⊆ u a
simp only [subset_def, mem_iUnion]
case refine'_4.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)
case refine'_4
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
⊢ ∀ (a : ι) (x : X), (∃ i i_1, x ∈ t i) → x ∈ u a
rintro i x ⟨a, rfl, hxa⟩
no goals
case refine'_4.intro.intro
ι : Type u
X : Type v
Y : Type w
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen (u a)
uc : (⋃ (i : ι), u i) = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), Set.Finite {i | Set.Nonempty (t i ∩ U x)}
x : X
a : α
hxa : x ∈ t a
⊢ x ∈ u (ind a)
exact hind _ hxa