Theorem: MapClusterPt.prod (Ray/Misc/Topology.lean)

State before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : MapClusterPt b a f
ga : Tendsto g a (𝓝 c)
⊢ MapClusterPt (b, c) a fun x => (f x, g x)
Tactic:
rw [mapClusterPt_iff] at fa ⊢
State after:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
⊢ ∀ s ∈ 𝓝 (b, c), ∃ᶠ (a : A) in a, (f a, g a) ∈ s

State before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
⊢ ∀ s ∈ 𝓝 (b, c), ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
intro s n
State after:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s

State before:
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
rcases mem_nhds_prod_iff.mp n with ⟨u, un, v, vn, sub⟩
State after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s

State before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∃ᶠ (a : A) in a, (f a, g a) ∈ s
Tactic:
apply (fa _ un).mp
State after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, f x ∈ u → (f x, g x) ∈ s

State before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, f x ∈ u → (f x, g x) ∈ s
Tactic:
apply (Filter.tendsto_iff_forall_eventually_mem.mp ga v vn).mp
State after:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, g x ∈ v → f x ∈ u → (f x, g x) ∈ s

State before:
case intro.intro.intro.intro
A B C : Type
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace C
f : A → B
g : A → C
a : Filter A
b : B
c : C
fa : ∀ s ∈ 𝓝 b, ∃ᶠ (a : A) in a, f a ∈ s
ga : Tendsto g a (𝓝 c)
s : Set (B × C)
n : s ∈ 𝓝 (b, c)
u : Set B
un : u ∈ 𝓝 b
v : Set C
vn : v ∈ 𝓝 c
sub : u ×ˢ v ⊆ s
⊢ ∀ᶠ (x : A) in a, g x ∈ v → f x ∈ u → (f x, g x) ∈ s
Tactic:
exact eventually_of_forall fun x gv fu ↦ sub (mk_mem_prod fu gv)
State after:
no goals