extend_comp

Mathlib.Topology.ContinuousMap.Bounded.Basic

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.extend_comp

English

The extended map composed with the embedding equals the original map g.

Русский

Расширенное отображение, образованное через вложение, равно исходному отображению g.

LaTeX

$$$\\text{extend}(f,g,h) \\circ f = g$$$

Lean4

@[simp]
nonrec theorem extend_comp (f : α ↪ δ) (g : α →ᵇ β) (h : δ →ᵇ β) : extend f g h ∘ f = g :=
  extend_comp f.injective _ _

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

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

Разделы

Аффилиация

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