Theorems · Definition

Function.extend

{α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α → β) → (α → γ) → (β → γ) → β → γ

Extension of a function g : α → γ along a function f : α → β. For every a : α, f a is sent to g a. f might not be surjective, so we use an auxiliary function j : β → γ by sending b : β not in the range of f to j b. If you do not care about the behavior outside the range, j can be used as a junk value by setting it to be 0 or Classical.arbitrary (assuming γ is nonempty). This definition is mathematically meaningful only when f a₁ = f a₂ → g a₁ = g a₂ (spelled g.FactorsThrough f). In particular this holds if f is injective. A typical use case is extending a function from a subtype to the entire type. If you wish to extend g : {b : β // p b} → γ to a function β → γ, you should use Function.extend Subtype.val g j.

Defined in

Mathlib.Logic.Function.Basic

Cited by

111 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 46 definitions · uses propext, Classical.choice, Quot.sound