mkD_of_not_continuousOn

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.mkD_of_not_continuousOn

← MathLib Explorer

English

If f is not continuous on s, mkD(s.restrict f) g = g.

Русский

Если f не непрерывна на s, mkD(s.restrict f) g = g.

LaTeX

$$$mkD(s.restrict f) g = g \quad\text{when } \neg ContinuousOn(f,s)$$$

Lean4

theorem mkD_of_not_continuousOn {s : Set α} {f : α → β} {g : C(s, β)} (hf : ¬ContinuousOn f s) :
    mkD (s.restrict f) g = g := by
  rw [continuousOn_iff_continuous_restrict] at hf
  exact mkD_of_not_continuous hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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