τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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')
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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')
simp only [omegaLimit_def, mem_iInter, MapsTo]
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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')
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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')
intro y hy u hu
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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'
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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')
refine' map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_image2_iff.2 fun t ht x hx ↦ _)
no goals
τ : Type u_3
α : Type u_4
β : Type u_5
ι : Type ?u.24430
inst✝¹ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
β' : Type u_2
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'
calc
  gb (ϕ t x) = ϕ' t (ga x) := ht.2 hx
  _ ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)