English
A local predicate on maps to T that extends continuousPrelocal, with a locality clause verifying continuity on refinements given by opens and their embeddings.
Русский
Локальное предикат на отображениях в T, который содержит непрерывность как предикат и проверяет непрерывность на локальных разбиениях по открытым подмножествам и вложениям.
LaTeX
$$$\\text{continuousLocal}(T) : \\text{LocalPredicate } (\\lambda x:. X \\to T) \\;\\text{with the same data as } \\text{continuousPrelocal}.$$$
Lean4
/-- Continuity is a "local" predicate on functions to a fixed topological space `T`.
-/
def continuousLocal (T) [TopologicalSpace T] : LocalPredicate fun _ : X ↦ T :=
{ continuousPrelocal X T with
locality := fun {U} f w ↦ by
apply continuous_iff_continuousAt.2
intro x
specialize w x
rcases w with ⟨V, m, i, w⟩
dsimp at w
rw [continuous_iff_continuousAt] at w
specialize w ⟨x, m⟩
simpa using (Opens.isOpenEmbedding_of_le i.le).continuousAt_iff.1 w }
