Theorems · Theorem

Function.extend_def

∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β)
  [inst : Decidable (∃ a, f a = b)],
  Function.extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b

Defined in

Mathlib.Logic.Function.Basic

Cited by

12 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Decidable