τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (s ∩ ϕ t ⁻¹' n)
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]
case mp
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)

case mpr
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
constructor
case mp
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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✝)
case mp
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
intro h _ hn _ hu
case mp.intro.intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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✝)
case mp
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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✝)
rcases h _ hu _ hn with ⟨_, _, _, _, ht, hx, hϕtx⟩
no goals
case mp.intro.intro.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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✝)
exact ⟨_, ht, _, hx, by rwa [mem_preimage, hϕtx]⟩
no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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✝
rwa [mem_preimage, hϕtx]
case mpr
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
case mpr
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
intro h _ hu _ hn
case mpr.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
case mpr
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
no goals
case mpr.intro.intro.intro.intro
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.28145
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)
exact ⟨_, hϕtx, _, _, ht, hx, rfl⟩