α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
hl : ∃ i, i ∈ s ∧ f i ∈ l
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
hl : ↑l ≤ 𝓟 (⋃ (i : ι) (_ : i ∈ s), f i)
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
rw [le_principal_iff, Ultrafilter.mem_coe, Ultrafilter.finite_biUnion_mem_iff hs] at hl
case intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
hl : ∃ i, i ∈ s ∧ f i ∈ l
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
rcases hl with ⟨i, his, hi⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
i : ι
his : i ∈ s
hi : f i ∈ l
x : α
hxi : x ∈ f i
hlx : ↑l ≤ 𝓝 x
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
case intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type u_1
π : ι → Type ?u.31333
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t : Set α
s : Set ι
f : ι → Set α
hs : Set.Finite s
hf : ∀ (i : ι), i ∈ s → IsCompact (f i)
l : Ultrafilter α
i : ι
his : i ∈ s
hi : f i ∈ l
x : α
hxi : x ∈ f i
hlx : ↑l ≤ 𝓝 x
⊢ ∃ a, (a ∈ ⋃ (i : ι) (_ : i ∈ s), f i) ∧ ↑l ≤ 𝓝 a
exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩