α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
⊢ ∀ (f : Ultrafilter (α × β)), ↑f ≤ 𝓟 (s ×ˢ t) → ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ×ˢ t)
rw [isCompact_iff_ultrafilter_le_nhds] at hs ht ⊢
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : ↑f ≤ 𝓟 (s ×ˢ t)
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
⊢ ∀ (f : Ultrafilter (α × β)), ↑f ≤ 𝓟 (s ×ˢ t) → ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
intro f hfs
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : ↑f ≤ 𝓟 (s ×ˢ t)
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
rw [le_principal_iff] at hfs
case intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : map Prod.fst ↑f ≤ 𝓝 a
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
obtain ⟨a : α, sa : a ∈ s, ha : map Prod.fst f.1 ≤ 𝓝 a⟩ :=
  hs (f.map Prod.fst) (le_principal_iff.2 <| mem_map.2 <| mem_of_superset hfs fun x => And.left)
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : map Prod.fst ↑f ≤ 𝓝 a
b : β
tb : b ∈ t
hb : map Prod.snd ↑f ≤ 𝓝 b
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
case intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : map Prod.fst ↑f ≤ 𝓝 a
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
obtain ⟨b : β, tb : b ∈ t, hb : map Prod.snd f.1 ≤ 𝓝 b⟩ :=
  ht (f.map Prod.snd) (le_principal_iff.2 <| mem_map.2 <| mem_of_superset hfs fun x => And.right)
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : map Prod.fst ↑f ≤ 𝓝 a
b : β
tb : b ∈ t
hb : map Prod.snd ↑f ≤ 𝓝 b
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
rw [map_le_iff_le_comap] at ha hb
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ↑f ≤ 𝓝 (a, b)
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ∃ a, a ∈ s ×ˢ t ∧ ↑f ≤ 𝓝 a
refine' ⟨⟨a, b⟩, ⟨sa, tb⟩, _⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ↑f ≤ 𝓝 a ×ˢ 𝓝 b
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ↑f ≤ 𝓝 (a, b)
rw [nhds_prod_eq]
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.96853
π : ι → Type ?u.96858
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s : Set α
t : Set β
hs : ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → ∃ a, a ∈ s ∧ ↑f ≤ 𝓝 a
ht : ∀ (f : Ultrafilter β), ↑f ≤ 𝓟 t → ∃ a, a ∈ t ∧ ↑f ≤ 𝓝 a
f : Ultrafilter (α × β)
hfs : s ×ˢ t ∈ ↑f
a : α
sa : a ∈ s
ha : ↑f ≤ comap Prod.fst (𝓝 a)
b : β
tb : b ∈ t
hb : ↑f ≤ comap Prod.snd (𝓝 b)
⊢ ↑f ≤ 𝓝 a ×ˢ 𝓝 b
exact le_inf ha hb