extend_of_isEmpty — Mathlib

English

If α is empty, then for any f : α → β, g : α → γ, h : β → γ, the extension satisfies Function.extend f g h = h.

Русский

Если α пуст, то для любых f : α → β, g : α → γ, h : β → γ выполняется Function.extend f g h = h.

LaTeX

$$Function.extend\_of\_isEmpty$$

Lean4

theorem extend_of_isEmpty [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) : Function.extend f g h = h :=
  funext fun _ ↦ (Function.extend_apply' _ _ _) fun ⟨a, _⟩ ↦ isEmptyElim a

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