extend_comp

Mathlib.Logic.Function.Basic

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

English

If f is injective, then extend f g e' ∘ f = g.

Русский

Если f инъективна, то extend f g e' после применения по f равен g.

LaTeX

$$$\operatorname{extend} f g e' \circ f = g \quad\text{при } \text{Injective}(f)$$$

Lean4

@[simp]
theorem extend_comp (hf : Injective f) (g : α → γ) (e' : β → γ) : extend f g e' ∘ f = g :=
  funext fun a ↦ hf.extend_apply g e' a

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

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

Разделы

Аффилиация

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