mkD_of_not_continuous

Mathlib.Topology.ContinuousMap.Basic

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

English

If f is not continuous, then mkD f g = g.

Русский

Если f не непрерывна, тогда mkD f g = g.

LaTeX

$$$\mkD f g = g \quad\text{when } \neg \operatorname{Continuous}(f)$$$

Lean4

theorem mkD_of_not_continuous {f : α → β} {g : C(α, β)} (hf : ¬Continuous f) : mkD f g = g := by
  simp only [mkD, hf, ↓reduceDIte]

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

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

Разделы

Аффилиация

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