# Miscellaneous function constructions and lemmas #

source
@[reducible]
def Function.eval {α : Sort u_1} {β : α → Sort u_4} (x : α) (f : (x : α) → β x) :
β x

Evaluate a function at an argument. Useful if you want to talk about the partially applied `Function.eval x : (∀ x, β x) → β x`.

Equations

- Function.eval x f = f x

Instances For

source
theorem Function.eval_apply {α : Sort u_1} {β : α → Sort u_4} (x : α) (f : (x : α) → β x) :
eval x f = f x
source
theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
(fun (x : α) => y) = const α y
source
theorem Function.const_injective {α : Sort u_1} {β : Sort u_2} [Nonempty α] :
Injective (const α)
source
@[simp]
theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [Nonempty α] {y₁ y₂ : β} :
const α y₁ = const α y₂ ↔ y₁ = y₂
source
theorem Function.onFun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α) :
onFun f g a b = f (g a) (g b)
source
theorem Function.hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), a ≍ a' → f a ≍ f' a') :
f ≍ f'
source
theorem Function.ne_iff {α : Sort u_1} {β : α → Sort u_4} {f₁ f₂ : (a : α) → β a} :
f₁ ≠ f₂ ↔ ∃ (a : α), f₁ a ≠ f₂ a
source
theorem Function.funext_iff_of_subsingleton {α : Sort u_1} {β : Sort u_2} {f : α → β} [Subsingleton α] {g : α → β} (x y : α) :
f x = g y ↔ f = g
source
theorem Function.swap_lt {α : Type u_4} [LT α] :
(swap fun (x1 x2 : α) => x1 < x2) = fun (x1 x2 : α) => x1 > x2
source
theorem Function.swap_le {α : Type u_4} [LE α] :
(swap fun (x1 x2 : α) => x1 ≤ x2) = fun (x1 x2 : α) => x1 ≥ x2
source
theorem Function.swap_gt {α : Type u_4} [LT α] :
(swap fun (x1 x2 : α) => x1 > x2) = fun (x1 x2 : α) => x1 < x2
source
theorem Function.swap_ge {α : Type u_4} [LE α] :
(swap fun (x1 x2 : α) => x1 ≥ x2) = fun (x1 x2 : α) => x1 ≤ x2
source
theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Bijective f) :
Injective f
source
theorem Function.Bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Bijective f) :
Surjective f
source
theorem Function.not_injective_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} :
¬Injective f ↔ ∃ (a : α), ∃ (b : α), f a = f b ∧ a ≠ b
source
def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : α → β} [DecidableEq β] (I : 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

source
theorem Function.Injective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Injective (f ∘ g)) :
Injective g
source
@[simp]
theorem Function.Injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (g : γ → α) :
Injective (f ∘ g) ↔ Injective g
source
theorem Function.Injective.of_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (I : Injective (f ∘ g)) (hg : Surjective g) :
Injective f
source
theorem Function.Surjective.bijective₂_of_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (hf : Surjective f) (hg : Surjective g) (I : Injective (f ∘ g)) :
Bijective f ∧ Bijective g
source
@[simp]
theorem Function.Injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Bijective g) :
Injective (f ∘ g) ↔ Injective f
source
theorem Function.Injective.piMap {ι : Sort u_4} {α : ι → Sort u_5} {β : ι → Sort u_6} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Injective (f i)) :
Injective (Pi.map f)
source
theorem Function.Injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : β → γ} (hg : Injective g) :
Injective fun (x : α → β) => g ∘ x

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

source
theorem Function.injective_comp_left_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [Nonempty α] {g : β → γ} :
(Injective fun (x : α → β) => g ∘ x) ↔ Injective g
source
theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : α → β) :
Injective f
source
theorem Function.bijective_of_subsingleton {α : Sort u_1} [Subsingleton α] (f : α → α) :
Bijective f
source
theorem Function.Injective.dite {α : Sort u_1} {β : Sort u_2} (p : α → Prop) [DecidablePred p] {f : { a : α // p a } → β} {f' : { a : α // ¬p a } → β} (hf : Injective f) (hf' : Injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩) :
Injective fun (x : α) => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩
source
theorem Function.Surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (S : Surjective (f ∘ g)) :
Surjective f
source
@[simp]
theorem Function.Surjective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Surjective g) :
Surjective (f ∘ g) ↔ Surjective f
source
theorem Function.Surjective.of_comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (S : Surjective (f ∘ g)) (hf : Injective f) :
Surjective g
source
theorem Function.Injective.bijective₂_of_surjective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α} (hf : Injective f) (hg : Injective g) (S : Surjective (f ∘ g)) :
Bijective f ∧ Bijective g
source
@[simp]
theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Bijective f) (g : γ → α) :
Surjective (f ∘ g) ↔ Surjective g
source
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) ⋯

source
theorem Function.Surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → Prop} :
(∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
source
theorem Function.Surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → β → Prop} :
(∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
source
theorem Function.Surjective.forall₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → β → β → Prop} :
(∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
source
theorem Function.Surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → Prop} :
(∃ (y : β), p y) ↔ ∃ (x : α), p (f x)
source
theorem Function.Surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → β → Prop} :
(∃ (y₁ : β), ∃ (y₂ : β), p y₁ y₂) ↔ ∃ (x₁ : α), ∃ (x₂ : α), p (f x₁) (f x₂)
source
theorem Function.Surjective.exists₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Surjective f) {p : β → β → β → Prop} :
(∃ (y₁ : β), ∃ (y₂ : β), ∃ (y₃ : β), p y₁ y₂ y₃) ↔ ∃ (x₁ : α), ∃ (x₂ : α), ∃ (x₃ : α), p (f x₁) (f x₂) (f x₃)
source
theorem Function.Surjective.injective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Surjective f) :
Injective fun (g : β → γ) => g ∘ f
source
theorem Function.injective_comp_right_iff_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {γ : Type u_4} [Nontrivial γ] :
(Injective fun (g : β → γ) => g ∘ f) ↔ Surjective f
source
theorem Function.Surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Surjective f) {g₁ g₂ : β → γ} :
g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂
source
theorem Function.surjective_of_right_cancellable_Prop {α : Sort u_1} {β : Sort u_2} {f : α → β} (h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂) :
Surjective f
source
theorem Function.bijective_iff_existsUnique {α : Sort u_1} {β : Sort u_2} (f : α → β) :
Bijective f ↔ ∀ (b : β), ∃! a : α, f a = b
source
theorem Function.Bijective.existsUnique {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Bijective f) (b : β) :
∃! a : α, f a = b

Shorthand for using projection notation with `Function.bijective_iff_existsUnique`.

source
theorem Function.Bijective.existsUnique_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : Bijective f) {p : β → Prop} :
(∃! y : β, p y) ↔ ∃! x : α, p (f x)
source
theorem Function.Bijective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : Bijective g) :
Bijective (f ∘ g) ↔ Bijective f
source
theorem Function.Bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Bijective f) (g : γ → α) :
Bijective (f ∘ g) ↔ Bijective g
source
theorem Function.cantor_surjective {α : Type u_4} (f : α → Set α) :
¬Surjective f

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

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

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

source
theorem Function.not_surjective_Type {α : Type u} (f : α → Type (max u v)) :
¬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.

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

`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

source
theorem Function.isPartialInv_left {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : IsPartialInv f g) (x : α) :
g (f x) = some x
source
theorem Function.injective_of_isPartialInv {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : IsPartialInv f g) :
Injective f
source
theorem Function.injective_of_isPartialInv_right {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α} (H : IsPartialInv f g) (x y : β) (b : α) (h₁ : b ∈ g x) (h₂ : b ∈ g y) :
x = y
source
theorem Function.LeftInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) :
f ∘ g = id
source
theorem Function.leftInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
LeftInverse f g ↔ f ∘ g = id
source
theorem Function.RightInverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : RightInverse f g) :
g ∘ f = id
source
theorem Function.rightInverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
RightInverse f g ↔ g ∘ f = id
source
theorem Function.LeftInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : LeftInverse f g) (hh : LeftInverse h i) :
LeftInverse (h ∘ f) (g ∘ i)
source
theorem Function.RightInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β} (hf : RightInverse f g) (hh : RightInverse h i) :
RightInverse (h ∘ f) (g ∘ i)
source
theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : LeftInverse g f) :
RightInverse f g
source
theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : RightInverse g f) :
LeftInverse f g
source
theorem Function.LeftInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) :
Surjective f
source
theorem Function.RightInverse.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : RightInverse f g) :
Injective f
source
theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) (hf : Injective f) :
RightInverse f g
source
theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : LeftInverse f g) (hg : Surjective g) :
RightInverse f g
source
theorem Function.RightInverse.leftInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
RightInverse f g → Surjective f → LeftInverse f g
source
theorem Function.RightInverse.leftInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
RightInverse f g → Injective g → LeftInverse f g
source
theorem Function.LeftInverse.eq_rightInverse {α : Sort u_1} {β : Sort u_2} {f : α → β} {g₁ g₂ : β → α} (h₁ : LeftInverse g₁ f) (h₂ : RightInverse g₂ f) :
g₁ = g₂
source
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

source
theorem Function.partialInv_of_injective {α : Type u_4} {β : Sort u_5} {f : α → β} (I : Injective f) :
IsPartialInv f (partialInv f)
source
theorem Function.partialInv_left {α : Type u_4} {β : Sort u_5} {f : α → β} (I : Injective f) (x : α) :
partialInv f (f x) = some x
source
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

source
theorem Function.invFun_eq {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {b : β} (h : ∃ (a : α), f a = b) :
f (invFun f b) = b
source
theorem Function.apply_invFun_apply {α : Type u_3} {β : Type u_4} {f : α → β} {a : α} :
f (invFun f (f a)) = f a
source
theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {b : β} (h : ¬∃ (a : α), f a = b) :
invFun f b = Classical.choice inst✝
source
theorem Function.invFun_eq_of_injective_of_rightInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} {g : β → α} (hf : Injective f) (hg : RightInverse g f) :
invFun f = g
source
theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Surjective f) :
RightInverse (invFun f) f
source
theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Injective f) :
LeftInverse (invFun f) f
source
theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Injective f) :
Surjective (invFun f)
source
theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Injective f) :
invFun f ∘ f = id
source
theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} (hf : Injective f) :
HasLeftInverse f
source
theorem Function.injective_iff_hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : α → β} :
Injective f ↔ HasLeftInverse f
source
noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : 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

source
theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : α → β} (h : Surjective f) (b : β) :
f (surjInv h b) = b
source
@[simp]
theorem Function.comp_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Surjective f) :
f ∘ surjInv hf = id
source
theorem Function.rightInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Surjective f) :
RightInverse (surjInv hf) f
source
theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : α → β} (hf : Bijective f) :
LeftInverse (surjInv ⋯) f
source
theorem Function.Surjective.hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} (hf : Surjective f) :
HasRightInverse f
source
theorem Function.surjective_iff_hasRightInverse {α : Sort u} {β : Sort v} {f : α → β} :
Surjective f ↔ HasRightInverse f
source
theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : α → β} :
Bijective f ↔ ∃ (g : β → α), LeftInverse g f ∧ RightInverse g f
source
theorem Function.injective_surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : Surjective f) :
Injective (surjInv h)
source
theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : Nonempty α] [Subsingleton β] (f : α → β) :
Surjective f
source
theorem Function.Surjective.piMap {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Surjective (f i)) :
Surjective (Pi.map f)
source
theorem Function.Surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : Surjective g) :
Surjective fun (x : α → β) => g ∘ x

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

source
theorem Function.surjective_comp_left_iff {α : Sort u} {β : Sort v} {γ : Sort w} [Nonempty α] {g : β → γ} :
(Surjective fun (x : α → β) => g ∘ x) ↔ Surjective g
source
theorem Function.Bijective.piMap {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), Bijective (f i)) :
Bijective (Pi.map f)
source
theorem Function.Bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : β → γ} (hg : Bijective g) :
Bijective fun (x : α → β) => g ∘ x

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

source
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

source
@[simp]
theorem Function.update_self {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a) :
update f a v a = v
source
@[simp]
theorem Function.update_of_ne {α : Sort u} {β : α → Sort v} [DecidableEq α] {a a' : α} (h : a ≠ a') (v : β a') (f : (a : α) → β a) :
update f a' v a = f a
source
theorem Function.update_apply {α : Sort u} [DecidableEq α] {β : Sort u_1} (f : α → β) (a' : α) (b : β) (a : α) :
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`

source
theorem Function.update_eq_const_of_subsingleton {α : Sort u} {α' : Sort w} [DecidableEq α] [Subsingleton α] (a : α) (v : α') (f : α → α') :
update f a v = const α v
source
theorem Function.surjective_eval {α : Sort u} {β : α → Sort v} [h : ∀ (a : α), Nonempty (β a)] (a : α) :
Surjective (eval a)
source
theorem Function.update_injective {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) :
Injective (update f a')
source
theorem Function.forall_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop) :
(∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
source
theorem Function.exists_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β a → Prop) :
(∃ (x : α), p x (update f a b x)) ↔ p a b ∨ ∃ (x : α), x ≠ a ∧ p x (f x)
source
theorem Function.update_eq_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a} :
update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
source
theorem Function.eq_update_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {a : α} {b : β a} {f g : (a : α) → β a} :
g = update f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x
source
@[simp]
theorem Function.update_eq_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
update f a b = f ↔ b = f a
source
@[simp]
theorem Function.eq_update_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
f = update f a b ↔ f a = b
source
theorem Function.ne_update_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
f ≠ update f a b ↔ f a ≠ b
source
theorem Function.update_ne_self_iff {α : Sort u} {β : α → Sort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
update f a b ≠ f ↔ b ≠ f a
source
@[simp]
theorem Function.update_eq_self {α : Sort u} {β : α → Sort v} [DecidableEq α] (a : α) (f : (a : α) → β a) :
update f a (f a) = f
source
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 : α') => update g i a (f j)) = fun (j : α') => g (f j)
source
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) :
update g i a ∘ f = g ∘ f

Non-dependent version of `Function.update_comp_eq_of_forall_ne'`

source
theorem Function.update_comp_eq_of_injective' {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α] [DecidableEq α'] (g : (a : α) → β a) {f : α' → α} (hf : Injective f) (i : α') (a : β (f i)) :
(fun (j : α') => update g (f i) a (f j)) = update (fun (i : α') => g (f i)) i a
source
theorem Function.update_apply_of_injective {α : Sort u} {β : α → Sort v} {α' : Sort w} [DecidableEq α] [DecidableEq α'] (g : (a : α) → β a) {f : α' → α} (hf : Injective f) (i : α') (a : β (f i)) (j : α') :
update g (f i) a (f j) = update (fun (i : α') => g (f i)) i a j
source
theorem Function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [DecidableEq α] [DecidableEq α'] {β : Sort u_1} (g : α' → β) {f : α → α'} (hf : Injective f) (i : α) (a : β) :
update g (f i) a ∘ f = update (g ∘ f) i a

Non-dependent version of `Function.update_comp_eq_of_injective'`

source
theorem Function.rec_update {ι : Sort u_1} {κ : Sort u_2} {α : κ → Sort u_3} [DecidableEq ι] [DecidableEq κ] {ctor : ι → κ} (hctor : Injective ctor) (recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i) (h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i) (h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k) (f : (i : ι) → α (ctor i)) (i : ι) (x : α (ctor i)) :
recursor (update f i x) = update (recursor f) (ctor i) x

Recursors can be pushed inside `Function.update`.

The `ctor` argument should be a one-argument constructor like `Sum.inl`, and `recursor` should be an inductive recursor partially applied in all but that constructor, such as `(Sum.rec · g)`.

In future, we should build some automation to generate applications like `Option.rec_update` for all inductive types.

source
@[simp]
theorem Option.rec_update {α : Type u_1} {β : Option α → Sort u_2} [DecidableEq α] (f : β none) (g : (a : α) → β (some a)) (a : α) (x : β (some a)) :
(fun (t : Option α) => rec f (Function.update g a x) t) = Function.update (fun (t : Option α) => rec f g t) (some a) x
source
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 (update g i v j) = update (fun (k : ι) => f k (g k)) i (f i v) j
source
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 (update g i v j) (update h i w j) = update (fun (k : ι) => f k (g k) (h k)) i (f i v w) j
source
theorem Function.pred_update {α : Sort u} {β : α → Sort v} [DecidableEq α] (P : ⦃a : α⦄ → β a → Prop) (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)
source
theorem Function.comp_update {α : Sort u} [DecidableEq α] {α' : Sort u_1} {β : Sort u_2} (f : α' → β) (g : α → α') (i : α) (v : α') :
f ∘ update g i v = update (f ∘ g) i (f v)
source
theorem Function.update_comm {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a b : α} (h : a ≠ b) (v : β a) (w : β b) (f : (a : α) → β a) :
update (update f a v) b w = update (update f b w) a v
source
@[simp]
theorem Function.update_idem {α : Sort u_2} [DecidableEq α] {β : α → Sort u_1} {a : α} (v w : β a) (f : (a : α) → β a) :
update (update f a v) a w = update f a w
source
@[simp]
theorem Pi.map_update {ι : Sort u_1} [DecidableEq ι] {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i} (g : (i : ι) → α i) (i : ι) (a : α i) :
Pi.map f (Function.update g i a) = Function.update (Pi.map f g) i (f i a)
source
@[simp]
theorem Pi.map_injective {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} [∀ (i : ι), Nonempty (α i)] {f : (i : ι) → α i → β i} :
Function.Injective (Pi.map f) ↔ ∀ (i : ι), Function.Injective (f i)
source
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

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

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

source
theorem Function.extend_def {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : α → γ) (e' : β → γ) (b : β) [Decidable (∃ (a : α), f a = b)] :
extend f g e' b = if h : ∃ (a : α), f a = b then g (Classical.choose h) else e' b
source
theorem Function.Injective.factorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (g : α → γ) :
FactorsThrough g f
source
theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ} (hf : FactorsThrough g f) (e' : β → γ) (a : α) :
extend f g e' (f a) = g a
source
@[simp]
theorem Function.Injective.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (g : α → γ) (e' : β → γ) (a : α) :
extend f g e' (f a) = g a
source
@[simp]
theorem Function.extend_apply' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ (a : α), f a = b) :
extend f g e' b = e' b
source
@[simp]
theorem Function.extend_id {α : Sort u_1} {γ : Sort u_3} (g e' : α → γ) :
extend id g e' = g
source
theorem Function.Injective.extend_comp {γ : Sort u_3} {α₁ : Sort u_4} {α₂ : Sort u_5} {α₃ : Sort u_6} {f₁₂ : α₁ → α₂} (h₁₂ : Injective f₁₂) {f₂₃ : α₂ → α₃} (h₂₃ : Injective f₂₃) (g : α₁ → γ) (e' : α₃ → γ) :
extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e'
source
theorem Function.factorsThrough_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) [Nonempty γ] :
FactorsThrough g f ↔ ∃ (e : β → γ), g = e ∘ f
source
theorem Function.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {g : α → γ} (F : γ → δ) (f : α → β) (e' : β → γ) (b : β) :
F (extend f g e' b) = extend f (F ∘ g) (F ∘ e') b
source
theorem Function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (e' : β → γ) :
Injective fun (g : α → γ) => extend f g e'
source
theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ} (e' : β → γ) (hf : FactorsThrough g f) :
extend f g e' ∘ f = g
source
@[simp]
theorem Function.extend_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (c : γ) :
(extend f (fun (x : α) => c) fun (x : β) => c) = fun (x : β) => c
source
@[simp]
theorem Function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (g : α → γ) (e' : β → γ) :
extend f g e' ∘ f = g
source
theorem Function.Injective.surjective_comp_right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Injective f) (g₀ : β → γ) :
Surjective fun (g : β → γ) => g ∘ f
source
theorem Function.Injective.surjective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} [Nonempty γ] (hf : Injective f) :
Surjective fun (g : β → γ) => g ∘ f
source
theorem Function.surjective_comp_right_iff_injective {α : Sort u_1} {β : Sort u_2} {f : α → β} {γ : Type u_4} [Nontrivial γ] :
(Surjective fun (g : β → γ) => g ∘ f) ↔ Injective f
source
theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : Bijective f) :
Bijective fun (g : β → γ) => g ∘ f
source
theorem Function.FactorsThrough.rfl {α : Sort u_1} {β : Sort u_2} {f : α → β} :
FactorsThrough f f
source
theorem Function.FactorsThrough.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : γ → δ) :
FactorsThrough (g' ∘ g) f
source
theorem Function.FactorsThrough.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : δ → α) :
FactorsThrough (g ∘ g') (f ∘ g')
source
theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) :
uncurry f = fun (p : α × β) => f p.fst p.snd
source
theorem Function.uncurry_injective {α : Type u_1} {β : Type u_2} {γ : Sort u_3} :
Injective uncurry
source
theorem Function.curry_injective {α : Type u_1} {β : Type u_2} {γ : Sort u_3} :
Injective curry
source
theorem Function.uncurry_flip {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) :
uncurry (flip f) = uncurry f ∘ Prod.swap
source
theorem Function.flip_curry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) :
flip (curry f) = curry (f ∘ Prod.swap)
source
theorem Function.curry_update {α : Type u_1} {α' : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq α'] (f : α × α' → β) (aa' : α × α') (b : β) :
curry (update f aa' b) = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b)
source
theorem Function.uncurry_update_update {α : Type u_1} {α' : Type u_2} {β : Type u_3} [DecidableEq α] [DecidableEq α'] (f : α → α' → β) (a : α) (a' : α') (b : β) :
uncurry (update f a (update (f a) a' b)) = update (uncurry f) (a, a') b
source
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

source
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

source
theorem Function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ) (g : γ → δ) :
uncurry (bicompr g f) = g ∘ uncurry f
source
theorem Function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (g : α → γ) (h : β → δ) :
uncurry (bicompl f g h) = uncurry f ∘ Prod.map g h
source
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

source
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↿_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↿") (Lean.ParserDescr.cat `term 1024))

Instances For

source
instance Function.hasUncurryBase {α : Type u_1} {β : Type u_2} :
HasUncurry (α → β) α β
Equations

- Function.hasUncurryBase = { uncurry := id }

source
instance Function.hasUncurryInduction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [HasUncurry β γ δ] :
HasUncurry (α → β) (α × γ) δ
Equations

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

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

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

Equations

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

Instances For

source
theorem Bool.involutive_not :
Function.Involutive not
source
@[simp]
theorem Function.Involutive.comp_self {α : Sort u} {f : α → α} (h : Involutive f) :
f ∘ f = id
source
theorem Function.Involutive.leftInverse {α : Sort u} {f : α → α} (h : Involutive f) :
LeftInverse f f
source
theorem Function.Involutive.leftInverse_iff {α : Sort u} {f : α → α} (h : Involutive f) {g : α → α} :
LeftInverse g f ↔ g = f
source
theorem Function.Involutive.rightInverse {α : Sort u} {f : α → α} (h : Involutive f) :
RightInverse f f
source
theorem Function.Involutive.injective {α : Sort u} {f : α → α} (h : Involutive f) :
Injective f
source
theorem Function.Involutive.surjective {α : Sort u} {f : α → α} (h : Involutive f) :
Surjective f
source
theorem Function.Involutive.bijective {α : Sort u} {f : α → α} (h : Involutive f) :
Bijective f
source
theorem Function.Involutive.ite_not {α : Sort u} {f : α → α} (h : 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`.

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

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

source
theorem Function.not_involutive :
Involutive Not
source
theorem Function.not_injective :
Injective Not
source
theorem Function.not_surjective :
Surjective Not
source
theorem Function.not_bijective :
Bijective Not
source
@[simp]
theorem Function.symmetric_apply_eq_iff {α : Sort u_1} {f : α → α} :
(Symmetric fun (x1 x2 : α) => f x1 = x2) ↔ Involutive f
source
def Function.Injective2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) :
Prop

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

source
theorem Function.Injective2.left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Injective2 f) (b : β) :
Injective fun (a : α) => f a b

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

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

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

source
theorem Function.Injective2.uncurry {α : Type u_4} {β : Type u_5} {γ : Type u_6} {f : α → β → γ} (hf : Injective2 f) :
Injective (uncurry f)
source
theorem Function.Injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Injective2 f) [Nonempty β] :
Injective f

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

source
theorem Function.Injective2.right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Injective2 f) [Nonempty α] :
Injective fun (b : β) (a : α) => f a b

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

source
theorem Function.Injective2.eq_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ} (hf : Injective2 f) {a₁ a₂ : α} {b₁ b₂ : β} :
f a₁ b₁ = f a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂
source
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

source
theorem Function.sometimes_eq {p : Prop} {α : Sort u_1} [Nonempty α] (f : p → α) (a : p) :
sometimes f = f a
source
theorem Function.sometimes_spec {p : Prop} {α : Sort u_1} [Nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) :
P (sometimes f)
source
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`.

source
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`.

source
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`.

source
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`.

source
def Set.piecewise {α : Type u} {β : α → Sort v} (s : Set α) (f 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` #

source
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
source
theorem eq_mp_bijective {α β : Sort u_3} (h : α = β) :
Function.Bijective h.mp
source
theorem eq_mpr_bijective {α β : Sort u_3} (h : α = β) :
Function.Bijective h.mpr
source
theorem cast_bijective {α β : 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.

source
@[simp]
theorem eq_rec_inj {α : Sort u_1} {a a' : α} (h : a = a') {C : α → Type u_3} (x y : C a) :
h ▸ x = h ▸ y ↔ x = y
source
@[simp]
theorem cast_inj {α β : Type u} (h : α = β) {x y : α} :
cast h x = cast h y ↔ x = y
source
theorem Function.LeftInverse.eq_rec_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
⋯ ▸ C (g (f a)) = C a
source
theorem Function.LeftInverse.eq_rec_on_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
Eq.recOn ⋯ (C (g (f a))) = C a
source
theorem Function.LeftInverse.cast_eq {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
cast ⋯ (C (g (f a))) = C a
source
def Set.SeparatesPoints {α : Type u_3} {β : Type u_4} (A : Set (α → β)) :
Prop

A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.

Equations

- A.SeparatesPoints = ∀ ⦃x y : α⦄, x ≠ y → ∃ (f : α → β), f ∈ A ∧ f x ≠ f y

Instances For

source
theorem InvImage.equivalence {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Equivalence r) :
Equivalence (InvImage r f)
source
instance instDecidableUncurryOfFstSnd_mathlib {α : Type u_3} {β : Type u_4} {r : α → β → Prop} {x : α × β} [Decidable (r x.fst x.snd)] :
Decidable (Function.uncurry r x)
Equations

- instDecidableUncurryOfFstSnd_mathlib = inst✝

source
instance instDecidableCurryOfMk_mathlib {α : Type u_3} {β : Type u_4} {r : α × β → Prop} {a : α} {b : β} [Decidable (r (a, b))] :
Decidable (Function.curry r a b)
Equations

- instDecidableCurryOfMk_mathlib = inst✝

source
@[simp]
theorem Pi.map_id {ι : Type u_3} {α : ι → Type u_4} :
(Pi.map fun (i : ι) => id) = id
source
@[simp]
theorem Pi.map_id' {ι : Type u_3} {α : ι → Type u_4} :
(Pi.map fun (i : ι) (a : α i) => a) = fun (x : (i : ι) → α i) => x
source
theorem Pi.map_comp_map {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} (f : (i : ι) → α i → β i) (g : (i : ι) → β i → γ i) :
Pi.map g ∘ Pi.map f = Pi.map fun (i : ι) => g i ∘ f i