seqContinuous

Mathlib.Topology.Sequences

URI: https://scilib.ai/kg/mathlib#Continuous.seqContinuous

English

A continuous function is sequentially continuous.

Русский

Функция непрерывна тогда и только тогда, когда она последовательночти непрерывна.

LaTeX

$$$\text{Continuous}(f) \Rightarrow \text{SeqContinuous}(f)$$$

Lean4

protected theorem seqContinuous {f : X → Y} (hf : Continuous f) : SeqContinuous f := fun _x p hx =>
  (hf.tendsto p).comp hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru