English
For any f: X → Y with Y pseudo-metrizable, the set {x | ContinuousAt f x} is a Gδ set.
Русский
Для любого отображения f: X → Y, где Y псевдометризируемо, множество {x | ContinuousAt f x} является множеством Gδ.
LaTeX
$$setOf_continuousAt [PseudoMetrizableSpace Y] (f : X → Y) : IsGδ {x | ContinuousAt f x}$$
Lean4
theorem setOf_continuousAt [PseudoMetrizableSpace Y] (f : X → Y) : IsGδ {x | ContinuousAt f x} :=
by
let _ := pseudoMetrizableSpacePseudoMetric Y
obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis
simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis, forall_prop_of_true, setOf_forall]
refine .iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_
rintro ⟨s, ⟨hsx, hso⟩, hsU⟩
filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩
