extend_apply'

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.extend_apply'

English

If x is outside the image of f, the extension uses h to define the value at x.

Русский

Если x не лежит в образе f, значение на x задаётся через h.

LaTeX

$$$Extend(f,g,h)(x) = h(x) \\quad\\text{if } x \\notin \\operatorname{range}(f)$$

Lean4

nonrec theorem extend_apply' {f : α ↪ δ} {x : δ} (hx : x ∉ range f) (g : α →ᵇ β) (h : δ →ᵇ β) : extend f g h x = h x :=
  extend_apply' _ _ _ hx

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

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

Разделы

Аффилиация

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