[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun t x => ϕ (m t) x) s ⊆ ω f₂ ϕ s
[PROOFSTEP]
refine' iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, _⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 (fun t x => ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
rw [← image2_image_left]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure (image2 ϕ ((fun t => m t) '' (m ⁻¹' u)) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')
[PROOFSTEP]
simp only [omegaLimit_def, mem_iInter, MapsTo]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
⊢ ∀ ⦃x : β⦄,
    (∀ (i : Set τ), i ∈ f → x ∈ closure (image2 ϕ i s)) → ∀ (i : Set τ), i ∈ f → gb x ∈ closure (image2 ϕ' i s')
[PROOFSTEP]
intro y hy u hu
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ (i : Set τ), i ∈ f → y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
⊢ gb y ∈ closure (image2 ϕ' u s')
[PROOFSTEP]
refine' map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_image2_iff.2 fun t ht x hx ↦ _)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
β' : Type u_6
inst✝ : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous gb
y : β
hy : ∀ (i : Set τ), i ∈ f → y ∈ closure (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x | (fun t => EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ gb (ϕ t x) ∈ image2 ϕ' u s'
[PROOFSTEP]
calc
  gb (ϕ t x) = ϕ' t (ga x) := ht.2 hx
  _ ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_5
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun t x => ϕ t (g x)) s
[PROOFSTEP]
simp only [omegaLimit, image2_image_right]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s ∩ ϕ t ⁻¹' n)
[PROOFSTEP]
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)) ↔
    ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
constructor
[GOAL]
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)) →
    ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
intro h _ hn _ hu
[GOAL]
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
⊢ ∃ x, x ∈ U✝ ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n✝)
[PROOFSTEP]
rcases h _ hu _ hn with ⟨_, _, _, _, ht, hx, hϕtx⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝² : β
left✝ : w✝² ∈ n✝
w✝¹ : τ
w✝ : α
ht : w✝¹ ∈ U✝
hx : w✝ ∈ s
hϕtx : ϕ w✝¹ w✝ = w✝²
⊢ ∃ x, x ∈ U✝ ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n✝)
[PROOFSTEP]
exact ⟨_, ht, _, hx, by rwa [mem_preimage, hϕtx]⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝² : β
left✝ : w✝² ∈ n✝
w✝¹ : τ
w✝ : α
ht : w✝¹ ∈ U✝
hx : w✝ ∈ s
hϕtx : ϕ w✝¹ w✝ = w✝²
⊢ w✝ ∈ ϕ w✝¹ ⁻¹' n✝
[PROOFSTEP]
rwa [mem_preimage, hϕtx]
[GOAL]
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)) →
    ∀ (i : Set τ), i ∈ f → ∀ (t : Set β), t ∈ 𝓝 y → Set.Nonempty (t ∩ image2 ϕ i s)
[PROOFSTEP]
intro h _ hu _ hn
[GOAL]
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
⊢ Set.Nonempty (t✝ ∩ image2 ϕ i✝ s)
[PROOFSTEP]
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
[GOAL]
case mpr.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
h : ∀ (n : Set β), n ∈ 𝓝 y → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (s ∩ ϕ x ⁻¹' n)
i✝ : Set τ
hu : i✝ ∈ f
t✝ : Set β
hn : t✝ ∈ 𝓝 y
w✝¹ : τ
ht : w✝¹ ∈ i✝
w✝ : α
hx : w✝ ∈ s
hϕtx : w✝ ∈ ϕ w✝¹ ⁻¹' t✝
⊢ Set.Nonempty (t✝ ∩ image2 ϕ i✝ s)
[PROOFSTEP]
exact ⟨_, hϕtx, _, _, ht, hx, rfl⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (ϕ t '' s ∩ n)
[PROOFSTEP]
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
x : α
y : β
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun t => ϕ t x
[PROOFSTEP]
simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff, singleton_inter_nonempty, mem_preimage]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
⊢ ω f ϕ (s₁ ∪ s₂) = ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
ext y
[GOAL]
case h
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
constructor
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
[PROOFSTEP]
simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty, frequently_or_distrib]
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ (∀ (n : Set β),
      n ∈ 𝓝 y → (∃ᶠ (x : τ) in f, Set.Nonempty (s₁ ∩ ϕ x ⁻¹' n)) ∨ ∃ᶠ (x : τ) in f, Set.Nonempty (s₂ ∩ ϕ x ⁻¹' n)) →
    (∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s₁ ∩ ϕ t ⁻¹' n)) ∨
      ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s₂ ∩ ϕ t ⁻¹' n)
[PROOFSTEP]
contrapose!
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ ((∃ n, n ∈ 𝓝 y ∧ ¬∃ᶠ (t : τ) in f, Set.Nonempty (s₁ ∩ ϕ t ⁻¹' n)) ∧
      ∃ n, n ∈ 𝓝 y ∧ ¬∃ᶠ (t : τ) in f, Set.Nonempty (s₂ ∩ ϕ t ⁻¹' n)) →
    ∃ n, n ∈ 𝓝 y ∧ (¬∃ᶠ (x : τ) in f, Set.Nonempty (s₁ ∩ ϕ x ⁻¹' n)) ∧ ¬∃ᶠ (x : τ) in f, Set.Nonempty (s₂ ∩ ϕ x ⁻¹' n)
[PROOFSTEP]
simp only [not_frequently, not_nonempty_iff_eq_empty, ← subset_empty_iff]
[GOAL]
case h.mp
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ ((∃ n, n ∈ 𝓝 y ∧ ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∃ n, n ∈ 𝓝 y ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅) →
    ∃ n, n ∈ 𝓝 y ∧ (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
[PROOFSTEP]
rintro ⟨⟨n₁, hn₁, h₁⟩, ⟨n₂, hn₂, h₂⟩⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
⊢ ∃ n, n ∈ 𝓝 y ∧ (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
[PROOFSTEP]
refine' ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ _, h₂.mono fun t ↦ _⟩
[GOAL]
case h.mp.intro.intro.intro.intro.intro.refine'_1
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
case h.mp.intro.intro.intro.intro.intro.refine'_2
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
[PROOFSTEP]
exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_left _ _,
  Subset.trans <| inter_subset_inter_right _ <| preimage_mono <| inter_subset_right _ _]
[GOAL]
case h.mpr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
[PROOFSTEP]
rintro (hy | hy)
[GOAL]
case h.mpr.inl
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₁
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)
case h.mpr.inr
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₂
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)
[PROOFSTEP]
exacts [omegaLimit_mono_right _ _ (subset_union_left _ _) hy, omegaLimit_mono_right _ _ (subset_union_right _ _) hy]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ⋃ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
[PROOFSTEP]
rw [iUnion_subset_iff]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
[PROOFSTEP]
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
[PROOFSTEP]
rw [omegaLimit_eq_biInter_inter _ _ _ hv]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ (u : Set τ) (_ : u ∈ f), closure (image2 ϕ (u ∩ v) s) = ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u ∩ v) s)
[PROOFSTEP]
apply biInter_eq_iInter
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
rw [omegaLimit_eq_iInter]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s) ⊆ closure (image2 ϕ u s)
[PROOFSTEP]
intro _ hx
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ (u : ↑f.sets), closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
[PROOFSTEP]
rw [mem_iInter] at hx 
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
[PROOFSTEP]
exact hx ⟨u, hu⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rcases hc₂ with ⟨v, hv₁, hv₂⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
let k := closure (image2 ϕ v s)
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hk : IsCompact (k \ n) := IsCompact.diff (isCompact_of_isClosed_subset hc₁ isClosed_closure hv₂) hn₁
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
let j u := (closure (image2 ϕ (u ∩ v) s))ᶜ
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
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₂
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rw [this, diff_subset_comm, diff_iUnion]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂ 
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
simp_rw [diff_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rw [← inter_iInter]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact Subset.trans (inter_subset_right _ _) hn₂
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
let w := (⋂ u ∈ g, u) ∩ v
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hw₂ : w ∈ f := by simpa [*]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
simpa [*]
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
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
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))ᶜ
[PROOFSTEP]
apply Subset.trans hg₃
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))ᶜ
[PROOFSTEP]
simp only [iUnion_subset_iff, compl_subset_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
intros u hu
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
mono
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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_1
α : Type u_2
β : Type u_3
ι : Type u_4
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_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
refine' iInter_subset_of_subset u (iInter_subset_of_subset hu _)
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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_1
α : Type u_2
β : Type u_3
ι : Type u_4
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_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
all_goals exact Subset.rfl
[GOAL]
case h.hs.h₁
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case h.hs.h₂
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case h.ht
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact Subset.rfl
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ :=
  by
  simp only [compl_subset_compl]
  exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))ᶜ
[PROOFSTEP]
simp only [compl_subset_compl]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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ᶜ
[PROOFSTEP]
rw [union_comm, ← inter_subset, diff_eq, inter_comm]
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
have hw : closure (image2 ϕ w s) ⊆ n := compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact ⟨_, hw₂, hw⟩
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
[PROOFSTEP]
rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁ hc₂ hn₁ hn₂ with
  ⟨u, hu_mem, hu⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
[PROOFSTEP]
refine' mem_of_superset hu_mem fun t ht x hx ↦ _
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ n
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n
[PROOFSTEP]
exact hu (subset_closure <| mem_image2_of_mem ht hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
[PROOFSTEP]
rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ with ⟨u, hu_mem, hu⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
[PROOFSTEP]
refine' mem_of_superset hu_mem fun t ht x hx ↦ _
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
inst✝ : CompactSpace β
v : Set β
hv₁ : IsOpen v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure (image2 ϕ u s) ⊆ v
t : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v
[PROOFSTEP]
exact hu (subset_closure <| mem_image2_of_mem ht hx)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
rcases hc₂ with ⟨v, hv₁, hv₂⟩
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
[GOAL]
case intro.intro
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
apply IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed
[GOAL]
case intro.intro.hZd
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
[GOAL]
case intro.intro.hZd.mk.mk
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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)
[PROOFSTEP]
use⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
[GOAL]
case h
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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) })
[PROOFSTEP]
constructor
[GOAL]
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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 h.right
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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) })
[PROOFSTEP]
all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
case h.left
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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) })
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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₁ }
[PROOFSTEP]
simp
[GOAL]
case h.right
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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) })
[PROOFSTEP]
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)
[GOAL]
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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₂ }
[PROOFSTEP]
simp
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
intro u
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
have hn : (image2 ϕ (u ∩ v) s).Nonempty := Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
[GOAL]
case intro.intro.hZn
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
exact hn.mono subset_closure
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
intro
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
apply isCompact_of_isClosed_subset hc₁ isClosed_closure
[GOAL]
case intro.intro.hZc
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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
[PROOFSTEP]
calc
  _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset (inter_subset_right _ _) Subset.rfl)
  _ ⊆ c := hv₂
[GOAL]
case intro.intro.hZcl
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
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))
[PROOFSTEP]
exact fun _ ↦ isClosed_closure
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)
[PROOFSTEP]
refine' fun t ↦ MapsTo.mono_right _ (omegaLimit_subset_of_tendsto ϕ s (hf t))
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
t : τ
⊢ MapsTo (toFun ϕ t) (ω f ϕ.toFun s) (ω f (fun t_1 x => toFun ϕ ((fun x x_1 => x + x_1) t t_1) x) s)
[PROOFSTEP]
exact mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm) (continuous_const.flow ϕ continuous_id)
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f ϕ.toFun (toFun ϕ t '' s) ⊆ ω f ϕ.toFun s
[PROOFSTEP]
simp only [omegaLimit_image_eq, ← map_add]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddMonoid τ
inst✝¹ : ContinuousAdd τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun x => x + t) f f
⊢ ω f (fun t_1 x => toFun ϕ (t_1 + t) x) s ⊆ ω f ϕ.toFun s
[PROOFSTEP]
exact omegaLimit_subset_of_tendsto ϕ s ht
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => x + t) f f
t : τ
⊢ ω f ϕ.toFun s = ω f ϕ.toFun (toFun ϕ (-t) '' (toFun ϕ t '' s))
[PROOFSTEP]
simp [image_image, ← map_add]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s
[PROOFSTEP]
simp only [subset_def, mem_omegaLimit_iff_frequently₂, frequently_iff]
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
⊢ ∀ (x : α),
    (∀ (n : Set α), n ∈ 𝓝 x → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)) →
      ∀ (n : Set α), n ∈ 𝓝 x → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
intro _ h
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
⊢ ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rintro n hn u hu
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩
[GOAL]
case intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases h o (IsOpen.mem_nhds ho₂ ho₃) hu with ⟨t, _ht₁, ht₂⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₁ : (ω f ϕ s ∩ o).Nonempty :=
  ht₂.mono (inter_subset_inter_left _ ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
  l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_fw_image _ _ _ hu hb.1, hb.2⟩
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
have l₃ : (o ∩ image2 ϕ u s).Nonempty := by
  rcases l₂ with ⟨b, hb₁, hb₂⟩
  exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)
[GOAL]
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
⊢ Set.Nonempty (o ∩ image2 ϕ.toFun u s)
[PROOFSTEP]
rcases l₂ with ⟨b, hb₁, hb₂⟩
[GOAL]
case intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
b : α
hb₁ : b ∈ closure (image2 ϕ.toFun u s)
hb₂ : b ∈ o
⊢ Set.Nonempty (o ∩ image2 ϕ.toFun u s)
[PROOFSTEP]
exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)
[GOAL]
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
l₃ : Set.Nonempty (o ∩ image2 ϕ.toFun u s)
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
rcases l₃ with ⟨ϕra, ho, ⟨_, _, hr, ha, hϕra⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : TopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto ((fun x x_1 => x + x_1) t) f f
x✝ : α
h : ∀ (n : Set α), n ∈ 𝓝 x✝ → ∀ {U : Set τ}, U ∈ f → ∃ x, x ∈ U ∧ Set.Nonempty (toFun ϕ x '' ω f ϕ.toFun s ∩ n)
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : Set.Nonempty (toFun ϕ t '' ω f ϕ.toFun s ∩ o)
l₁ : Set.Nonempty (ω f ϕ.toFun s ∩ o)
l₂ : Set.Nonempty (closure (image2 ϕ.toFun u s) ∩ o)
ϕra : α
ho : ϕra ∈ o
w✝¹ : τ
w✝ : α
hr : w✝¹ ∈ u
ha : w✝ ∈ s
hϕra : toFun ϕ w✝¹ w✝ = ϕra
⊢ ∃ x, x ∈ u ∧ Set.Nonempty (toFun ϕ x '' s ∩ n)
[PROOFSTEP]
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩
