ι : Type u_5
κ : Type ?u.123707
X : Type u_3
Y : Type ?u.123713
Z : Type ?u.123716
α : Type u_4
β : Type ?u.123722
γ : Type ?u.123725
𝓕 : Type ?u.123728
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_1
κ₂ : Type u_2
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
ι : Type u_5
κ : Type ?u.123707
X : Type u_3
Y : Type ?u.123713
Z : Type ?u.123716
α : Type u_4
β : Type ?u.123722
γ : Type ?u.123725
𝓕 : Type ?u.123728
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_1
κ₂ : Type u_2
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
  hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
ι : Type u_5
κ : Type ?u.123707
X : Type u_3
Y : Type ?u.123713
Z : Type ?u.123716
α : Type u_4
β : Type ?u.123722
γ : Type ?u.123725
𝓕 : Type ?u.123728
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_1
κ₂ : Type u_2
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α (s₂ ib)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
ι : Type u_5
κ : Type ?u.123707
X : Type u_3
Y : Type ?u.123713
Z : Type ?u.123716
α : Type u_4
β : Type ?u.123722
γ : Type ?u.123725
𝓕 : Type ?u.123728
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_1
κ₂ : Type u_2
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun ∘ Function.swap F) x ∈
                  {g | ((↑UniformFun.ofFun ∘ Function.swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
simp only [Function.comp_apply, mem_setOf_eq, exists_prop]
no goals
ι : Type u_5
κ : Type ?u.123707
X : Type u_3
Y : Type ?u.123713
Z : Type ?u.123716
α : Type u_4
β : Type ?u.123722
γ : Type ?u.123725
𝓕 : Type ?u.123728
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
κ₁ : Type u_1
κ₂ : Type u_2
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : HasBasis (𝓝 x₀) p₁ s₁
hα : HasBasis (𝓤 α) p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia,
          p₁ ia ∧
            ∀ (x : X),
              x ∈ s₁ ia →
                (↑UniformFun.ofFun (Function.swap F x₀), ↑UniformFun.ofFun (Function.swap F x)) ∈
                  UniformFun.gen ι α (s₂ ib)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
rfl