α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
⊢ UniformCauchySeqOnFilter F p p'
intro u hu
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
have := tendsto_swap4_prod.eventually ((hF t ht).prod_mk (hF t ht))
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (x : (ι × ι) × α),
    (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd) ∈
          t ∧
        (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd) ∈
          t →
      (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.fst.fst m.snd, F m.fst.snd m.snd) ∈ u
apply this.diag_of_prod_right.mono
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (x : (ι × ι) × α),
    (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).fst.snd) ∈
          t ∧
        (f
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd,
            F
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.fst
              (((x.fst, x.snd, x.snd).fst.fst, (x.fst, x.snd, x.snd).snd.fst), (x.fst, x.snd, x.snd).fst.snd,
                    (x.fst, x.snd, x.snd).snd.snd).snd.snd) ∈
          t →
      (F x.fst.fst x.snd, F x.fst.snd x.snd) ∈ u
simp only [and_imp, Prod.forall]
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u
intro n1 n2 x hl hr
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).fst.snd) ∈
        t ∧
      (f ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd,
          F ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.fst
            ((x.fst.fst, x.snd.fst), x.fst.snd, x.snd.snd).snd.snd) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u
exact Set.mem_of_mem_of_subset (prod_mk_mem_compRel (htsymm hl) hr) htmem