case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v, v ∈ f ∧ closure (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
rcases hc₂ with ⟨v, hv₁, hv₂⟩
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
let k := closure (image2 ϕ v s)
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hk : IsCompact (k \ n) :=
  IsCompact.diff (isCompact_of_isClosed_subset hc₁ isClosed_closure hv₂) hn₁
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
let j u := closure (image2 ϕ (u ∩ v) s)ᶜ
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u := by
  have : (⋃ u ∈ f, j u) = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
  rw [this, diff_subset_comm, diff_iUnion]
  rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
  simp_rw [diff_compl]
  rw [← inter_iInter]
  exact Subset.trans (inter_subset_right _ _) hn₂
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
let w := (⋂ u ∈ g, u) ∩ v
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hw₂ : w ∈ f := by simpa [*]
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ := by
  apply Subset.trans hg₃
  simp only [iUnion_subset_iff, compl_subset_compl]
  intros u hu
  mono
  refine' iInter_subset_of_subset u (iInter_subset_of_subset hu _)
  all_goals exact Subset.rfl
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ := by
  simp only [compl_subset_compl]
  exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
hw : closure (image2 ϕ w s) ⊆ n
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
have hw : closure (image2 ϕ w s) ⊆ n :=
  compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
no goals
case intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
hw : closure (image2 ϕ w s) ⊆ n
⊢ ∃ u, u ∈ f ∧ closure (image2 ϕ u s) ⊆ n
exact ⟨_, hw₂, hw⟩
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
⊢ k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
have : (⋃ u ∈ f, j u) = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), k \ j ↑i) ⊆ n
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
rw [this, diff_subset_comm, diff_iUnion]
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), k \ j ↑i) ⊆ n
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), k \ j ↑i) ⊆ n
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), closure (image2 ϕ v s) ∩ closure (image2 ϕ (↑i ∩ v) s)) ⊆ n
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), k \ j ↑i) ⊆ n
simp_rw [diff_compl]
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (closure (image2 ϕ v s) ∩ ⋂ (i : ↑f.sets), closure (image2 ϕ (↑i ∩ v) s)) ⊆ n
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (⋂ (i : ↑f.sets), closure (image2 ϕ v s) ∩ closure (image2 ϕ (↑i ∩ v) s)) ⊆ n
rw [← inter_iInter]
no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
v : Set τ
hn₂ : (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)) ⊆ n
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
this : (⋃ (u : Set τ) (_ : u ∈ f), j u) = ⋃ (u : ↑f.sets), j ↑u
⊢ (closure (image2 ϕ v s) ∩ ⋂ (i : ↑f.sets), closure (image2 ϕ (↑i ∩ v) s)) ⊆ n
exact Subset.trans (inter_subset_right _ _) hn₂
no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
⊢ w ∈ f
simpa [*]
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ (⋃ (i : Set τ) (_ : i ∈ g), j i) ⊆ closure (image2 ϕ w s)ᶜ
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ k \ n ⊆ closure (image2 ϕ w s)ᶜ
apply Subset.trans hg₃
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∀ (i : Set τ), i ∈ g → closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (i ∩ v) s)
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ (⋃ (i : Set τ) (_ : i ∈ g), j i) ⊆ closure (image2 ϕ w s)ᶜ
simp only [iUnion_subset_iff, compl_subset_compl]
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (u ∩ v) s)
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
⊢ ∀ (i : Set τ), i ∈ g → closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (i ∩ v) s)
intros u hu
case h.hs.h₁
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ (⋂ (u : Set τ) (_ : u ∈ g), u) ⊆ u

case h.hs.h₂
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v

case h.ht
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ (u ∩ v) s)
mono
case h.hs.h₁
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

case h.hs.h₂
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v

case h.ht
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
case h.hs.h₁
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ (⋂ (u : Set τ) (_ : u ∈ g), u) ⊆ u

case h.hs.h₂
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v

case h.ht
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
refine' iInter_subset_of_subset u (iInter_subset_of_subset hu _)
no goals
case h.hs.h₁
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

case h.hs.h₂
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ v ⊆ v

case h.ht
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
all_goals exact Subset.rfl
no goals
case h.ht
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
u : Set τ
hu : u ∈ g
⊢ s ⊆ s
exact Subset.rfl
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ v s)
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
⊢ kᶜ ⊆ closure (image2 ϕ w s)ᶜ
simp only [compl_subset_compl]
no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
⊢ closure (image2 ϕ ((⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v) s) ⊆ closure (image2 ϕ v s)
exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.37681
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
k : Set β := closure (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u => closure (image2 ϕ (u ∩ v) s)ᶜ
hj₁ : ∀ (u : Set τ), u ∈ f → IsOpen (j u)
hj₂ : k \ n ⊆ ⋃ (u : Set τ) (_ : u ∈ f), j u
g : Set (Set τ)
hg₁ : ∀ (u : Set τ), u ∈ g → u ∈ f
hg₂ : Set.Finite g
hg₃ : k \ n ⊆ ⋃ (i : Set τ) (_ : i ∈ g), j i
w : Set τ := (⋂ (u : Set τ) (_ : u ∈ g), u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ closure (image2 ϕ w s)ᶜ
hw₄ : kᶜ ⊆ closure (image2 ϕ w s)ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ
rw [union_comm, ← inter_subset, diff_eq, inter_comm]