case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | ContinuousAt f x}
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
⊢ IsGδ {x | ContinuousAt f x}
obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric β _).exists_antitone_subbasis
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | Tendsto (fun x => (f x.fst, f x.snd)) (𝓝 x ×ˢ 𝓝 x) (uniformity β)}
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | ContinuousAt f x}
simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ), {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U i})
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | Tendsto (fun x => (f x.fst, f x.snd)) (𝓝 x ×ˢ 𝓝 x) (uniformity β)}
simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis, forall_prop_of_true,
  setOf_forall, id]
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
⊢ x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} →
    {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ), {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U i})
refine' isGδ_iInter fun k => IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x => _
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
s : Set α
hsU : ∀ (x : α × α), x ∈ s ×ˢ s → (f x.fst, f x.snd) ∈ U k
hsx : x ∈ s
hso : IsOpen s
⊢ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
⊢ x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} →
    {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
rintro ⟨s, ⟨hsx, hso⟩, hsU⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.13373
ι : Type ?u.13376
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
s : Set α
hsU : ∀ (x : α × α), x ∈ s ×ˢ s → (f x.fst, f x.snd) ∈ U k
hsx : x ∈ s
hso : IsOpen s
⊢ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
filter_upwards [IsOpen.mem_nhds hso hsx]with _ hy using⟨s, ⟨hy, hso⟩, hsU⟩