case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K

α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
tfae_have 1 → 2
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v

α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
tfae_have 2 → 3
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s

α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
tfae_3_to_1 : (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
tfae_have 3 → 1
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
tfae_3_to_1 : (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
⊢ List.TFAE
    [TendstoLocallyUniformlyOn G g p s, ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
      ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v]
tfae_finish
case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
h : TendstoLocallyUniformlyOn G g p s
K : Set α
hK1 : K ⊆ s
hK2 : IsCompact K
⊢ TendstoUniformlyOn G g p K
case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
⊢ TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
rintro h K hK1 hK2
no goals
case tfae_1_to_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
h : TendstoLocallyUniformlyOn G g p s
K : Set α
hK1 : K ⊆ s
hK2 : IsCompact K
⊢ TendstoUniformlyOn G g p K
exact (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
⊢ (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
rintro h x hx
case tfae_2_to_3.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
case tfae_2_to_3
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
no goals
case tfae_2_to_3.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
h : ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
K : Set α
hK3 : K ⊆ s
hK1 : K ∈ 𝓝 x
hK2 : IsCompact K
⊢ ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
refine' ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
⊢ (∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v) → TendstoLocallyUniformlyOn G g p s
rintro h u hu x hx
case tfae_3_to_1.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
case tfae_3_to_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
obtain ⟨v, hv1, hv2⟩ := h x hx
no goals
case tfae_3_to_1.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p✝ : Filter ι
p' : Filter α
g✝ : ι → α
inst✝¹ : TopologicalSpace α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 :
  (∀ (K : Set α), K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K) →
    ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
h : ∀ (x : α), x ∈ s → ∃ v, v ∈ 𝓝[s] x ∧ TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
v : Set α
hv1 : v ∈ 𝓝[s] x
hv2 : TendstoUniformlyOn G g p v
⊢ ∃ t, t ∈ 𝓝[s] x ∧ ∀ᶠ (n : ι) in p, ∀ (y : α), y ∈ t → (g y, G n y) ∈ u
exact ⟨v, hv1, hv2 u hu⟩