ContinuousOn — Mathlib

English

A function f: X → Y is continuous on a set s if it is continuous at every point of s within s.

Русский

Функция f: X → Y непрерывна на множестe s, если она непрерывна в каждой точке x ∈ s относительно s.

LaTeX

$$$\forall x \in s, \operatorname{ContinuousWithinAt}(f,s,x)$$$

Lean4

/-- A function between topological spaces is continuous on a subset `s`
when it's continuous at every point of `s` within `s`. -/
@[fun_prop]
def ContinuousOn (f : X → Y) (s : Set X) : Prop :=
  ∀ x ∈ s, ContinuousWithinAt f s x

Похожие утверждения