mkD_of_not_zero

Mathlib.Topology.ContinuousMap.ContinuousMapZero

URI: https://scilib.ai/kg/mathlib#ContinuousMapZero.mkD_of_not_zero

← MathLib Explorer

English

If f(0) ≠ 0, then mkD f g = g; the mkD construction collapses when the value at 0 is nonzero.

Русский

Если f(0) ≠ 0, то mkD f g = g; конструкция mkD исчезает, если значение в нуле не нулевое.

LaTeX

$$mkD(f,g) = g$$

Lean4

theorem mkD_of_not_zero [Zero X] {f : X → R} {g : C(X, R)₀} (hf : f 0 ≠ 0) : mkD f g = g := by
  simp only [mkD, not_and_of_not_right _ hf, ↓reduceDIte]

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

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

Разделы

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

Аффилиация

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