English
Continuity defines a prelocal predicate on maps into a fixed space T: a map is continuous, and restrictions to open embeddings remain continuous after composition.
Русский
Непрерывность задаёт пре-предикат над отображениями в фиксированное пространство T: функция непрямая, и ограничения на открытые вложения сохраняют непрерывность после композиции.
LaTeX
$$$\\text{continuousPrelocal}(T) := \\text{PrelocalPredicate } (\\lambda x: T)\\;\\text{with } \\text{pred } f := \\text{Continuous}(f), \\text{res } i\\; h := \\text{Continuous}(\\, h \\circ i \\,).$$$
Lean4
/-- Continuity is a "prelocal" predicate on functions to a fixed topological space `T`.
-/
@[simps!]
def continuousPrelocal (T) [TopologicalSpace T] : PrelocalPredicate fun _ : X ↦ T
where
pred {_} f := Continuous f
res {_ _} i _ h := Continuous.comp h (Opens.isOpenEmbedding_of_le i.le).continuous
