case intro.intro
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (ω f ϕ s)
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v, v ∈ f ∧ closure (image2 ϕ v s) ⊆ c
hs : Set.Nonempty s
⊢ Set.Nonempty (ω f ϕ s)
rcases hc₂ with ⟨v, hv₁, hv₂⟩
case intro.intro
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s))
case intro.intro
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (ω f ϕ s)
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
case intro.intro.hZd
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => closure (image2 ϕ (↑i ∩ v) s)

case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), Set.Nonempty (closure (image2 ϕ (↑i ∩ v) s))

case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))

case intro.intro.hZcl
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed (closure (image2 ϕ (↑i ∩ v) s))
case intro.intro
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Set.Nonempty (⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s))
apply IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z)
case intro.intro.hZd
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ Directed (fun x x_1 => x ⊇ x_1) fun i => closure (image2 ϕ (↑i ∩ v) s)
rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) }) ∧
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ∃ z,
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z) ∧
      (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
        ((fun i => closure (image2 ϕ (↑i ∩ v) s)) z)
use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
case intro.intro.hZd.mk.mk.left
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })

case intro.intro.hZd.mk.mk.right
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) }) ∧
    (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
      ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
constructor
no goals
case intro.intro.hZd.mk.mk.left
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁, property := hu₁ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })

case intro.intro.hZd.mk.mk.right
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
no goals
case intro.intro.hZd.mk.mk.right
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun x x_1 => x ⊇ x_1) ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₂, property := hu₂ })
    ((fun i => closure (image2 ϕ (↑i ∩ v) s)) { val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) })
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
no goals
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑{ val := u₁ ∩ u₂, property := (_ : u₁ ∩ u₂ ∈ f) } ⊆ ↑{ val := u₂, property := hu₂ }
simp
case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), Set.Nonempty (closure (image2 ϕ (↑i ∩ v) s))
intro u
case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
hn : Set.Nonempty (image2 ϕ (↑u ∩ v) s)
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
  Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
no goals
case intro.intro.hZn
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
u : ↑f.sets
hn : Set.Nonempty (image2 ϕ (↑u ∩ v) s)
⊢ Set.Nonempty (closure (image2 ϕ (↑u ∩ v) s))
exact hn.mono subset_closure
case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure (image2 ϕ (↑i✝ ∩ v) s))
case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure (image2 ϕ (↑i ∩ v) s))
intro
case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ closure (image2 ϕ (↑i✝ ∩ v) s) ⊆ c
case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ IsCompact (closure (image2 ϕ (↑i✝ ∩ v) s))
apply isCompact_of_isClosed_subset hc₁ isClosed_closure
no goals
case intro.intro.hZc
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
i✝ : ↑f.sets
⊢ closure (image2 ϕ (↑i✝ ∩ v) s) ⊆ c
calc
  _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
  _ ⊆ c := hv₂
no goals
case intro.intro.hZcl
τ : Type u_1
α : Type u_3
β : Type u_2
ι : Type ?u.74453
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : NeBot f
c : Set β
hc₁ : IsCompact c
hs : Set.Nonempty s
v : Set τ
hv₁ : v ∈ f
hv₂ : closure (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed (closure (image2 ϕ (↑i ∩ v) s))
exact fun _ ↦ isClosed_closure