Miscellaneous function constructions and lemmas #

theorem Function.eval_apply {α : Sort u_1} {β : α → Sort u_4} (x : α) (f : (x : α) → β x) :

Function.eval x f = f x

theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :

(fun (x : α) => y) = Function.const α y

theorem Function.const_injective {α : Sort u_1} {β : Sort u_2} [Nonempty α] :

Function.Injective (Function.const α)

@[simp]

theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [Nonempty α] {y₁ : β} {y₂ : β} :

Function.const α y₁ = Function.const α y₂ ↔ y₁ = y₂

theorem Function.onFun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a : α) (b : α) :

(f on g) a b = f (g a) (g b)

theorem Function.hfunext {α : Sort u} {α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), HEq a a' → HEq (f a) (f' a')) :

HEq f f'

theorem Function.ne_iff {α : Sort u_1} {β : α → Sort u_4} {f₁ : (a : α) → β a} {f₂ : (a : α) → β a} :

f₁ ≠ f₂ ↔ ∃ (a : α), f₁ a ≠ f₂ a

theorem Function.funext_iff_of_subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} [Subsingleton α] {g : α → β} (x : α) (y : α) :

f x = g y ↔ f = g

theorem Function.swap_lt {α : Type u_4} [Preorder α] :

(Function.swap fun (x1 x2 : α) => x1 < x2) = fun (x1 x2 : α) => x1 > x2

theorem Function.swap_le {α : Type u_4} [Preorder α] :

(Function.swap fun (x1 x2 : α) => x1 ≤ x2) = fun (x1 x2 : α) => x1 ≥ x2

theorem Function.swap_gt {α : Type u_4} [Preorder α] :

(Function.swap fun (x1 x2 : α) => x1 > x2) = fun (x1 x2 : α) => x1 < x2

theorem Function.swap_ge {α : Type u_4} [Preorder α] :

(Function.swap fun (x1 x2 : α) => x1 ≥ x2) = fun (x1 x2 : α) => x1 ≤ x2

theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) :

theorem Function.Bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) :

theorem Function.Injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : Function.Injective f) {a : α} {b : α} :

f a = f b ↔ a = b

theorem Function.Injective.beq_eq {α : Type u_4} {β : Type u_5} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β} (I : Function.Injective f) {a : α} {b : α} :

(f a == f b) = (a == b)

theorem Function.Injective.eq_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : Function.Injective f) {a : α} {b : α} {c : β} (h : f b = c) :

f a = c ↔ a = b

theorem Function.Injective.ne {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {a₁ : α} {a₂ : α} :

a₁ ≠ a₂ → f a₁ ≠ f a₂

theorem Function.Injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {x : α} {y : α} :

f x ≠ f y ↔ x ≠ y

theorem Function.Injective.ne_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Injective f) {x : α} {y : α} {z : β} (h : f y = z) :

f x ≠ z ↔ x ≠ y

theorem Function.not_injective_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} :

¬Function.Injective f ↔ ∃ (a : α), ∃ (b : α), f a = f b ∧ a ≠ b

def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : α → β} [DecidableEq β] (I : Function.Injective f) :

DecidableEq α

If the co-domain β of an injective function f : α → β has decidable equality, then the domain α also has decidable equality.

Equations

I.decidableEq x✝ x = decidable_of_iff (f x✝ = f x) ⋯

Instances For

theorem Function.Injective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Function.Injective (f ∘ g)) :

Function.Injective g

@[simp]

theorem Function.Injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : γ → α) :

Function.Injective (f ∘ g) ↔ Function.Injective g

theorem Function.Injective.of_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Function.Injective (f ∘ g)) (hg : Function.Surjective g) :

theorem Function.Surjective.bijective₂_of_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (hf : Function.Surjective f) (hg : Function.Surjective g) (I : Function.Injective (f ∘ g)) :

Function.Bijective f ∧ Function.Bijective g

@[simp]

theorem Function.Injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Function.Bijective g) :

Function.Injective (f ∘ g) ↔ Function.Injective f

theorem Function.Injective.piMap {ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Injective (f i)) :

Function.Injective (Pi.map f)

@[deprecated Function.Injective.piMap]

theorem Function.injective_pi_map {ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Injective (f i)) :

Function.Injective (Pi.map f)

Alias of Function.Injective.piMap.

theorem Function.Injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} (hg : Function.Injective g) :

Function.Injective fun (x : α → β) => g ∘ x

Composition by an injective function on the left is itself injective.

theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) :

theorem Function.Injective.dite {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [DecidablePred p] {f : { a : α // p a } → β} {f' : { a : α // ¬p a } → β} (hf : Function.Injective f) (hf' : Function.Injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) :

Function.Injective fun (x : α) => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩

theorem Function.Surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (S : Function.Surjective (f ∘ g)) :

@[simp]

theorem Function.Surjective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Function.Surjective g) :

Function.Surjective (f ∘ g) ↔ Function.Surjective f

theorem Function.Surjective.of_comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (S : Function.Surjective (f ∘ g)) (hf : Function.Injective f) :

Function.Surjective g

theorem Function.Injective.bijective₂_of_surjective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (hf : Function.Injective f) (hg : Function.Injective g) (S : Function.Surjective (f ∘ g)) :

Function.Bijective f ∧ Function.Bijective g

@[simp]

theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Bijective f) (g : γ → α) :

Function.Surjective (f ∘ g) ↔ Function.Surjective g

instance Function.decidableEqPFun (p : Prop) [Decidable p] (α : p → Type u_4) [(hp : p) → DecidableEq (α hp)] :

DecidableEq ((hp : p) → α hp)

Equations

Function.decidableEqPFun p α x✝ x = decidable_of_iff (∀ (hp : p), x✝ hp = x hp) ⋯

theorem Function.Surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → Prop} :

(∀ (y : β), p y) ↔ ∀ (x : α), p (f x)

theorem Function.Surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → β → Prop} :

(∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)

theorem Function.Surjective.forall₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → β → β → Prop} :

(∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)

theorem Function.Surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → Prop} :

(∃ (y : β), p y) ↔ ∃ (x : α), p (f x)

theorem Function.Surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → β → Prop} :

(∃ (y₁ : β), ∃ (y₂ : β), p y₁ y₂) ↔ ∃ (x₁ : α), ∃ (x₂ : α), p (f x₁) (f x₂)

theorem Function.Surjective.exists₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Surjective f) {p : β → β → β → Prop} :

(∃ (y₁ : β), ∃ (y₂ : β), ∃ (y₃ : β), p y₁ y₂ y₃) ↔ ∃ (x₁ : α), ∃ (x₂ : α), ∃ (x₃ : α), p (f x₁) (f x₂) (f x₃)

theorem Function.Surjective.injective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Surjective f) :

Function.Injective fun (g : β → γ) => g ∘ f

theorem Function.Surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Surjective f) {g₁ : β → γ} {g₂ : β → γ} :

g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂

theorem Function.surjective_of_right_cancellable_Prop {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂) :

theorem Function.bijective_iff_existsUnique {α : Sort u_1} {β : Sort u_2} (f : α → β) :

Function.Bijective f ↔ ∀ (b : β), ∃! a : α, f a = b

theorem Function.Bijective.existsUnique {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) (b : β) :

∃! a : α, f a = b

Shorthand for using projection notation with Function.bijective_iff_existsUnique.

theorem Function.Bijective.existsUnique_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Function.Bijective f) {p : β → Prop} :

(∃! y : β, p y) ↔ ∃! x : α, p (f x)

theorem Function.Bijective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Function.Bijective g) :

Function.Bijective (f ∘ g) ↔ Function.Bijective f

theorem Function.Bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Bijective f) (g : γ → α) :

Function.Bijective (f ∘ g) ↔ Function.Bijective g

theorem Function.cantor_surjective {α : Type u_4} (f : α → Set α) :

¬Function.Surjective f

Cantor's diagonal argument implies that there are no surjective functions from α to Set α.

theorem Function.cantor_injective {α : Type u_4} (f : Set α → α) :

¬Function.Injective f

Cantor's diagonal argument implies that there are no injective functions from Set α to α.

theorem Function.not_surjective_Type {α : Type u} (f : α → Type (max u v)) :

¬Function.Surjective f

There is no surjection from α : Type u into Type (max u v). This theorem demonstrates why Type : Type would be inconsistent in Lean.

def Function.IsPartialInv {α : Type u_4} {β : Sort u_5} (f : α → β) (g : β → Option α) :

g is a partial inverse to f (an injective but not necessarily surjective function) if g y = some x implies f x = y, and g y = none implies that y is not in the range of f.

Equations

Function.IsPartialInv f g = ∀ (x : α) (y : β), g y = some x ↔ f x = y

Instances For

theorem Function.isPartialInv_left {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) (x : α) :

g (f x) = some x

theorem Function.injective_of_isPartialInv {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) :

theorem Function.injective_of_isPartialInv_right {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : Function.IsPartialInv f g) (x : β) (y : β) (b : α) (h₁ : b ∈ g x) (h₂ : b ∈ g y) :

x = y

theorem Function.LeftInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) :

f ∘ g = id

theorem Function.leftInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

Function.LeftInverse f g ↔ f ∘ g = id

theorem Function.RightInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.RightInverse f g) :

g ∘ f = id

theorem Function.rightInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

Function.RightInverse f g ↔ g ∘ f = id

theorem Function.LeftInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : Function.LeftInverse f g) (hh : Function.LeftInverse h i) :

Function.LeftInverse (h ∘ f) (g ∘ i)

theorem Function.RightInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : Function.RightInverse f g) (hh : Function.RightInverse h i) :

Function.RightInverse (h ∘ f) (g ∘ i)

theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse g f) :

Function.RightInverse f g

theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.RightInverse g f) :

Function.LeftInverse f g

theorem Function.LeftInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) :

theorem Function.RightInverse.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.RightInverse f g) :

theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hf : Function.Injective f) :

Function.RightInverse f g

theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hg : Function.Surjective g) :

Function.RightInverse f g

theorem Function.RightInverse.leftInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

Function.RightInverse f g → Function.Surjective f → Function.LeftInverse f g

theorem Function.RightInverse.leftInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :

Function.RightInverse f g → Function.Injective g → Function.LeftInverse f g

theorem Function.LeftInverse.eq_rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g₁ : β → α} {g₂ : β → α} (h₁ : Function.LeftInverse g₁ f) (h₂ : Function.RightInverse g₂ f) :

g₁ = g₂

noncomputable def Function.partialInv {α : Type u_4} {β : Sort u_5} (f : α → β) (b : β) :

Option α

We can use choice to construct explicitly a partial inverse for a given injective function f.

Equations

Function.partialInv f b = if h : ∃ (a : α), f a = b then some (Classical.choose h) else none

Instances For

theorem Function.partialInv_of_injective {α : Type u_4} {β : Sort u_5} {f : α → β} (I : Function.Injective f) :

Function.IsPartialInv f (Function.partialInv f)

theorem Function.partialInv_left {α : Type u_4} {β : Sort u_5} {f : α → β} (I : Function.Injective f) (x : α) :

Function.partialInv f (f x) = some x

noncomputable def Function.invFun {α : Sort u} {β : Sort u_3} [Nonempty α] (f : α → β) :

β → α

The inverse of a function (which is a left inverse if f is injective and a right inverse if f is surjective).

Equations

Function.invFun f y = if h : ∃ (x : α), f x = y then h.choose else Classical.arbitrary α

Instances For

theorem Function.invFun_eq {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {b : β} (h : ∃ (a : α), f a = b) :

f (Function.invFun f b) = b

theorem Function.apply_invFun_apply {α : Type u_3} {β : Type u_4} {f : α → β} {a : α} :

f (Function.invFun f (f a)) = f a

theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {b : β} (h : ¬∃ (a : α), f a = b) :

Function.invFun f b = Classical.choice inst✝

theorem Function.invFun_eq_of_injective_of_rightInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {g : β → α} (hf : Function.Injective f) (hg : Function.RightInverse g f) :

Function.invFun f = g

theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Function.Surjective f) :

Function.RightInverse (Function.invFun f) f

theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.LeftInverse (Function.invFun f) f

theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.Surjective (Function.invFun f)

theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Function.Injective f) :

Function.invFun f ∘ f = id

Function.HasLeftInverse f

theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Function.Injective f) :

theorem Function.injective_iff_hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} :

Function.Injective f ↔ Function.HasLeftInverse f

noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) :

The inverse of a surjective function. (Unlike invFun, this does not require α to be inhabited.)

Equations

Function.surjInv h b = Classical.choose ⋯

Instances For

theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) :

f (Function.surjInv h b) = b

theorem Function.rightInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f) :

Function.RightInverse (Function.surjInv hf) f

theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Bijective f) :

Function.LeftInverse (Function.surjInv ⋯) f

Function.HasRightInverse f

theorem Function.Surjective.hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f) :

theorem Function.surjective_iff_hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} :

Function.Surjective f ↔ Function.HasRightInverse f

theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : α → β} :

Function.Bijective f ↔ ∃ (g : β → α), Function.LeftInverse g f ∧ Function.RightInverse g f

theorem Function.injective_surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) :

Function.Injective (Function.surjInv h)

theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : Nonempty α] [Subsingleton β] (f : α → β) :

theorem Function.Surjective.piMap {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Surjective (f i)) :

Function.Surjective (Pi.map f)

@[deprecated Function.Surjective.piMap]

theorem Function.surjective_pi_map {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Surjective (f i)) :

Function.Surjective (Pi.map f)

Alias of Function.Surjective.piMap.

theorem Function.Surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : Function.Surjective g) :

Function.Surjective fun (x : α → β) => g ∘ x

Composition by a surjective function on the left is itself surjective.

theorem Function.Bijective.piMap {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Bijective (f i)) :

Function.Bijective (Pi.map f)

@[deprecated Function.Bijective.piMap]

theorem Function.bijective_pi_map {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Function.Bijective (f i)) :

Function.Bijective (Pi.map f)

Alias of Function.Bijective.piMap.

theorem Function.Bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : Function.Bijective g) :

Function.Bijective fun (x : α → β) => g ∘ x

Composition by a bijective function on the left is itself bijective.

def Function.update {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :

β a

Replacing the value of a function at a given point by a given value.

Equations

Function.update f a' v a = if h : a = a' then ⋯ ▸ v else f a

Instances For

@[simp]

theorem Function.update_same {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a) :

Function.update f a v a = v

@[simp]

theorem Function.update_noteq {α : Sort u} {β : α → Sort v} [DecidableEq α] {a : α} {a' : α} (h : a ≠ a') (v : β a') (f : (a : α) → β a) :

Function.update f a' v a = f a

theorem Function.update_apply {α : Sort u} [DecidableEq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α) :

Function.update f a' b a = if a = a' then b else f a

On non-dependent functions, Function.update can be expressed as an ite

theorem Function.update_eq_const_of_subsingleton {α : Sort u} {α' : Sort w} [DecidableEq α] [Subsingleton α] (a : α) (v : α') (f : α → α') :

Function.update f a v = Function.const α v

theorem Function.surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), Nonempty (β a)] (a : α) :

Function.Surjective (Function.eval a)

theorem Function.update_injective {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) :

Function.Injective (Function.update f a')

theorem Function.forall_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop) :

(∀ (x : α), p x (Function.update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

theorem Function.exists_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop) :

(∃ (x : α), p x (Function.update f a b x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)

theorem Function.update_eq_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :

Function.update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x

theorem Function.eq_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :

g = Function.update f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x

@[simp]

theorem Function.update_eq_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :

Function.update f a b = f ↔ b = f a

@[simp]

theorem Function.eq_update_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :

f = Function.update f a b ↔ f a = b

theorem Function.ne_update_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :

f ≠ Function.update f a b ↔ f a ≠ b

theorem Function.update_ne_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :

Function.update f a b ≠ f ↔ b ≠ f a

@[simp]

theorem Function.update_eq_self {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α) (f : (a : α) → β a) :

Function.update f a (f a) = f

theorem Function.update_comp_eq_of_forall_ne' {α : Sort u} {β : α → Sort v} [DecidableEq α] {α' : Sort u_1} (g : (a : α) → β a) {f : α' → α} {i : α} (a : β i) (h : ∀ (x : α'), f x ≠ i) :

(fun (j : α') => Function.update g i a (f j)) = fun (j : α') => g (f j)

theorem Function.update_comp_eq_of_forall_ne {α' : Sort w} [DecidableEq α'] {α : Sort u_1} {β : Sort u_2} (g : α' → β) {f : α → α'} {i : α'} (a : β) (h : ∀ (x : α), f x ≠ i) :

Function.update g i a ∘ f = g ∘ f

Non-dependent version of Function.update_comp_eq_of_forall_ne'

theorem Function.update_comp_eq_of_injective' {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α] [DecidableEq α'] (g : (a : α) → β a) {f : α' → α} (hf : Function.Injective f) (i : α') (a : β (f i)) :

(fun (j : α') => Function.update g (f i) a (f j)) = Function.update (fun (i : α') => g (f i)) i a

theorem Function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [DecidableEq α] [DecidableEq α'] {β : Sort u_1} (g : α' → β) {f : α → α'} (hf : Function.Injective f) (i : α) (a : β) :

Function.update g (f i) a ∘ f = Function.update (g ∘ f) i a

Non-dependent version of Function.update_comp_eq_of_injective'

theorem Function.apply_update {ι : Sort u_1} [DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} (f : (i : ι) → α i → β i) (g : (i : ι) → α i) (i : ι) (v : α i) (j : ι) :

f j (Function.update g i v j) = Function.update (fun (k : ι) => f k (g k)) i (f i v) j

theorem Function.apply_update₂ {ι : Sort u_1} [DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {γ : ι → Sort u_4} (f : (i : ι) → α i → β i → γ i) (g : (i : ι) → α i) (h : (i : ι) → β i) (i : ι) (v : α i) (w : β i) (j : ι) :

f j (Function.update g i v j) (Function.update h i w j) = Function.update (fun (k : ι) => f k (g k) (h k)) i (f i v w) j

theorem Function.pred_update {α : Sort u} {β : α → Sort v} [DecidableEq α] (P : ⦃a : α⦄ → β a → Prop) (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :

P (Function.update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

theorem Function.comp_update {α : Sort u} [DecidableEq α] {α' : Sort u_1} {β : Sort u_2} (f : α' → β) (g : α → α') (i : α) (v : α') :

f ∘ Function.update g i v = Function.update (f ∘ g) i (f v)

theorem Function.update_comm {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a : α} {b : α} (h : a ≠ b) (v : β a) (w : β b) (f : (a : α) → β a) :

Function.update (Function.update f a v) b w = Function.update (Function.update f b w) a v

@[simp]

theorem Function.update_idem {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a : α} (v : β a) (w : β a) (f : (a : α) → β a) :

Function.update (Function.update f a v) a w = Function.update f a w

def Function.extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (j : β → γ) :

β → γ

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.

Equations

Function.extend f g j b = if h : ∃ (a : α), f a = b then g (Classical.choose h) else j b

Instances For

def Function.FactorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (g : α → γ) (f : α → β) :

g factors through f : f a = f b → g a = g b

Equations

Function.FactorsThrough g f = ∀ ⦃a b : α⦄, f a = f b → g a = g b

Instances For

theorem Function.extend_def {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [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

theorem Function.Injective.factorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : α → γ) :

Function.FactorsThrough g f

theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ} (hf : Function.FactorsThrough g f) (e' : β → γ) (a : α) :

Function.extend f g e' (f a) = g a

@[simp]

theorem Function.Injective.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : α → γ) (e' : β → γ) (a : α) :

Function.extend f g e' (f a) = g a

@[simp]

theorem Function.extend_apply' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ (a : α), f a = b) :

Function.extend f g e' b = e' b

theorem Function.factorsThrough_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) [Nonempty γ] :

Function.FactorsThrough g f ↔ ∃ (e : β → γ), g = e ∘ f

theorem Function.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β) :

F (Function.extend f g e' b) = Function.extend f (F ∘ g) (F ∘ e') b

theorem Function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (e' : β → γ) :

Function.Injective fun (g : α → γ) => Function.extend f g e'

theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ} (e' : β → γ) (hf : Function.FactorsThrough g f) :

Function.extend f g e' ∘ f = g

@[simp]

theorem Function.extend_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (c : γ) :

(Function.extend f (fun (x : α) => c) fun (x : β) => c) = fun (x : β) => c

@[simp]

theorem Function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g : α → γ) (e' : β → γ) :

Function.extend f g e' ∘ f = g

theorem Function.Injective.surjective_comp_right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Injective f) (g₀ : β → γ) :

Function.Surjective fun (g : β → γ) => g ∘ f

theorem Function.Injective.surjective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} [Nonempty γ] (hf : Function.Injective f) :

Function.Surjective fun (g : β → γ) => g ∘ f

theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Function.Bijective f) :

Function.Bijective fun (g : β → γ) => g ∘ f

theorem Function.FactorsThrough.rfl {α : Sort u_1} {β : Sort u_2} {f : α → β} :

Function.FactorsThrough f f

theorem Function.FactorsThrough.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ} (h : Function.FactorsThrough g f) (g' : γ → δ) :

Function.FactorsThrough (g' ∘ g) f

theorem Function.FactorsThrough.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ} (h : Function.FactorsThrough g f) (g' : δ → α) :

Function.FactorsThrough (g ∘ g') (f ∘ g')

theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) :

Function.uncurry f = fun (p : α × β) => f p.fst p.snd

@[simp]

theorem Function.uncurry_apply_pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (x : α) (y : β) :

Function.uncurry f (x, y) = f x y

@[simp]

theorem Function.curry_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β → γ) (x : α) (y : β) :

Function.curry f x y = f (x, y)

def Function.bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (g : α → γ) (h : β → δ) (a : α) (b : β) :

Compose a binary function f with a pair of unary functions g and h. If both arguments of f have the same type and g = h, then bicompl f g g = f on g.

Equations

Function.bicompl f g h a b = f (g a) (h b)

Instances For

def Function.bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ → δ) (g : α → β → γ) (a : α) (b : β) :

Compose a unary function f with a binary function g.

Equations

Function.bicompr f g a b = f (g a b)

Instances For

theorem Function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ) (g : γ → δ) :

Function.uncurry (Function.bicompr g f) = g ∘ Function.uncurry f

theorem Function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (g : α → γ) (h : β → δ) :

Function.uncurry (Function.bicompl f g h) = Function.uncurry f ∘ Prod.map g h

class Function.HasUncurry (α : Type u_5) (β : outParam (Type u_6)) (γ : outParam (Type u_7)) :

Type (max (max u_5 u_6) u_7)

Records a way to turn an element of α into a function from β to γ. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

uncurry : α → β → γ
Uncurrying operator. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Instances

def Function.«term↿_» :

Lean.ParserDescr

Uncurrying operator. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Equations

Function.«term↿_» = Lean.ParserDescr.node `Function.term↿_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1023))

Instances For

instance Function.hasUncurryBase {α : Type u_1} {β : Type u_2} :

Function.HasUncurry (α → β) α β

Equations

Function.hasUncurryBase = { uncurry := id }

instance Function.hasUncurryInduction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Function.HasUncurry β γ δ] :

Function.HasUncurry (α → β) (α × γ) δ

Equations

Function.hasUncurryInduction = { uncurry := fun (f : α → β) (p : α × γ) => (↿(f p.fst)) p.snd }

def Function.Involutive {α : Sort u_1} (f : α → α) :

A function is involutive, if f ∘ f = id.

Equations

Function.Involutive f = ∀ (x : α), f (f x) = x

Instances For

theorem Bool.involutive_not :

Function.Involutive not

@[simp]

theorem Function.Involutive.comp_self {α : Sort u} {f : α → α} (h : Function.Involutive f) :

f ∘ f = id

theorem Function.Involutive.leftInverse {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.LeftInverse f f

theorem Function.Involutive.leftInverse_iff {α : Sort u} {f : α → α} (h : Function.Involutive f) {g : α → α} :

Function.LeftInverse g f ↔ g = f

theorem Function.Involutive.rightInverse {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.RightInverse f f

theorem Function.Involutive.injective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

theorem Function.Involutive.surjective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

theorem Function.Involutive.bijective {α : Sort u} {f : α → α} (h : Function.Involutive f) :

Function.Bijective f

theorem Function.Involutive.ite_not {α : Sort u} {f : α → α} (h : Function.Involutive f) (P : Prop) [Decidable P] (x : α) :

f (if P then x else f x) = if ¬P then x else f x

Involuting an ite of an involuted value x : α negates the Prop condition in the ite.

theorem Function.Involutive.eq_iff {α : Sort u} {f : α → α} (h : Function.Involutive f) {x : α} {y : α} :

f x = y ↔ x = f y

An involution commutes across an equality. Compare to Function.Injective.eq_iff.

theorem Function.not_involutive :

Function.Involutive Not

theorem Function.not_injective :

Function.Injective Not

theorem Function.not_surjective :

Function.Surjective Not

theorem Function.not_bijective :

Function.Bijective Not

@[simp]

theorem Function.symmetric_apply_eq_iff {α : Sort u_1} {f : α → α} :

(Symmetric fun (x1 x2 : α) => f x1 = x2) ↔ Function.Involutive f

def Function.Injective2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) :

The property of a binary function f : α → β → γ being injective. Mathematically this should be thought of as the corresponding function α × β → γ being injective.

Equations

Function.Injective2 f = ∀ ⦃a₁ a₂ : α⦄ ⦃b₁ b₂ : β⦄, f a₁ b₁ = f a₂ b₂ → a₁ = a₂ ∧ b₁ = b₂

Instances For

theorem Function.Injective2.left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) (b : β) :

Function.Injective fun (a : α) => f a b

A binary injective function is injective when only the left argument varies.

theorem Function.Injective2.right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) (a : α) :

Function.Injective (f a)

A binary injective function is injective when only the right argument varies.

theorem Function.Injective2.uncurry {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β → γ} (hf : Function.Injective2 f) :

Function.Injective (Function.uncurry f)

theorem Function.Injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) [Nonempty β] :

As a map from the left argument to a unary function, f is injective.

theorem Function.Injective2.right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) [Nonempty α] :

Function.Injective fun (b : β) (a : α) => f a b

As a map from the right argument to a unary function, f is injective.

theorem Function.Injective2.eq_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Function.Injective2 f) {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :

f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

noncomputable def Function.sometimes {α : Sort u_1} {β : Sort u_2} [Nonempty β] (f : α → β) :

sometimes f evaluates to some value of f, if it exists. This function is especially interesting in the case where α is a proposition, in which case f is necessarily a constant function, so that sometimes f = f a for all a.

Equations

Function.sometimes f = if h : Nonempty α then f (Classical.choice h) else Classical.choice inst

Instances For

theorem Function.sometimes_eq {p : Prop} {α : Sort u_1} [Nonempty α] (f : p → α) (a : p) :

Function.sometimes f = f a

theorem Function.sometimes_spec {p : Prop} {α : Sort u_1} [Nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) :

P (Function.sometimes f)

theorem forall_existsUnique_iff {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} :

(∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), ∀ {a : α} {b : β}, r a b ↔ f a = b

A relation r : α → β → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some function f.

theorem forall_existsUnique_iff' {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop} :

(∀ (a : α), ∃! b : β, r a b) ↔ ∃ (f : α → β), r = fun (x1 : α) (x2 : β) => f x1 = x2

A relation r : α → β → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some function f.

theorem Symmetric.forall_existsUnique_iff' {α : Sort u_1} {r : α → α → Prop} (hr : Symmetric r) :

(∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Function.Involutive f ∧ r = fun (x1 x2 : α) => f x1 = x2

A symmetric relation r : α → α → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some involutive function f.

theorem Symmetric.forall_existsUnique_iff {α : Sort u_1} {r : α → α → Prop} (hr : Symmetric r) :

(∀ (a : α), ∃! b : α, r a b) ↔ ∃ (f : α → α), Function.Involutive f ∧ ∀ {a b : α}, r a b ↔ f a = b

A symmetric relation r : α → α → Prop is "function-like" (for each a there exists a unique b such that r a b) if and only if it is (f · = ·) for some involutive function f.

def Set.piecewise {α : Type u} {β : α → Sort v} (s : Set α) (f : (i : α) → β i) (g : (i : α) → β i) [(j : α) → Decidable (j ∈ s)] (i : α) :

β i

s.piecewise f g is the function equal to f on the set s, and to g on its complement.

Equations

s.piecewise f g i = if i ∈ s then f i else g i

Instances For

Bijectivity of `Eq.rec`, `Eq.mp`, `Eq.mpr`, and `cast` #

theorem eq_rec_on_bijective {α : Sort u_1} {C : α → Sort u_3} {a : α} {a' : α} (h : a = a') :

Function.Bijective fun (x : C a) => h ▸ x

theorem eq_mp_bijective {α : Sort u_3} {β : Sort u_3} (h : α = β) :

Function.Bijective h.mp

theorem eq_mpr_bijective {α : Sort u_3} {β : Sort u_3} (h : α = β) :

Function.Bijective h.mpr

theorem cast_bijective {α : Sort u_3} {β : Sort u_3} (h : α = β) :

Function.Bijective (cast h)

Note these lemmas apply to Type* not Sort*, as the latter interferes with simp, and is trivial anyway.

@[simp]

theorem eq_rec_inj {α : Sort u_1} {a : α} {a' : α} (h : a = a') {C : α → Type u_3} (x : C a) (y : C a) :

h ▸ x = h ▸ y ↔ x = y

@[simp]

theorem cast_inj {α : Type u} {β : Type u} (h : α = β) {x : α} {y : α} :

cast h x = cast h y ↔ x = y

theorem Function.LeftInverse.eq_rec_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :

⋯ ▸ C (g (f a)) = C a

theorem Function.LeftInverse.eq_rec_on_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :

Eq.recOn ⋯ (C (g (f a))) = C a