Miscellaneous function constructions and lemmas
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
@[simp]
theorem
function.eval_apply
{α : Sort u}
{β : α → Sort u_1}
(x : α)
(f : Π (x : α), β x) :
function.eval x f = f x
theorem
function.comp_apply
{α : Sort u}
{β : Sort v}
{φ : Sort w}
(f : β → φ)
(g : α → β)
(a : α) :
@[simp]
theorem
function.injective.eq_iff
{α : Sort u}
{β : Sort v}
{f : α → β}
(I : function.injective f)
{a b : α} :
theorem
function.injective.eq_iff'
{α : Sort u}
{β : Sort v}
{f : α → β}
(I : function.injective f)
{a b : α}
{c : β} :
theorem
function.injective.ne
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.injective f)
{a₁ a₂ : α} :
theorem
function.injective.ne_iff
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.injective f)
{x y : α} :
theorem
function.injective.ne_iff'
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.injective f)
{x y : α}
{z : β} :
If the co-domain β of an injective function f : α → β has decidable equality, then
the domain α also has decidable equality.
Equations
- I.decidable_eq = λ (a b : α), decidable_of_iff (f a = f b) _
theorem
function.injective.of_comp
{α : Sort u}
{β : Sort v}
{f : α → β}
{γ : Sort w}
{g : γ → α} :
function.injective (f ∘ g) → function.injective g
theorem
function.surjective.of_comp
{α : Sort u}
{β : Sort v}
{f : α → β}
{γ : Sort w}
{g : γ → α} :
function.surjective (f ∘ g) → function.surjective f
@[instance]
def
function.decidable_eq_pfun
(p : Prop)
[decidable p]
(α : p → Type u_1)
[Π (hp : p), decidable_eq (α hp)] :
decidable_eq (Π (hp : p), α hp)
Equations
- function.decidable_eq_pfun p α f g = decidable_of_iff (∀ (hp : p), f hp = g hp) _
theorem
function.surjective.forall
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.surjective f)
{p : β → Prop} :
(∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
theorem
function.surjective.forall₂
{α : Sort u}
{β : Sort v}
{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}
{β : Sort v}
{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}
{β : Sort v}
{f : α → β}
(hf : function.surjective f)
{p : β → Prop} :
(∃ (y : β), p y) ↔ ∃ (x : α), p (f x)
theorem
function.surjective.exists₂
{α : Sort u}
{β : Sort v}
{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}
{β : Sort v}
{f : α → β}
(hf : function.surjective f)
{p : β → β → β → Prop} :
(∃ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∃ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
Cantor's diagonal argument implies that there are no surjective functions from α
to set α.
Cantor's diagonal argument implies that there are no injective functions from set α to α.
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.is_partial_inv f g = ∀ (x : α) (y : β), g y = option.some x ↔ f x = y
theorem
function.is_partial_inv_left
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : β → option α}
(H : function.is_partial_inv f g)
(x : α) :
g (f x) = option.some x
theorem
function.injective_of_partial_inv
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : β → option α} :
theorem
function.injective_of_partial_inv_right
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : β → option α}
(H : function.is_partial_inv f g)
(x y : β)
(b : α) :
theorem
function.left_inverse.comp_eq_id
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.left_inverse f g → f ∘ g = id
theorem
function.left_inverse_iff_comp
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.left_inverse f g ↔ f ∘ g = id
theorem
function.right_inverse.comp_eq_id
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.right_inverse f g → g ∘ f = id
theorem
function.right_inverse_iff_comp
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.right_inverse f g ↔ g ∘ f = id
theorem
function.left_inverse.comp
{α : Sort u}
{β : Sort v}
{γ : Sort u_1}
{f : α → β}
{g : β → α}
{h : β → γ}
{i : γ → β} :
function.left_inverse f g → function.left_inverse h i → function.left_inverse (h ∘ f) (g ∘ i)
theorem
function.right_inverse.comp
{α : Sort u}
{β : Sort v}
{γ : Sort u_1}
{f : α → β}
{g : β → α}
{h : β → γ}
{i : γ → β} :
function.right_inverse f g → function.right_inverse h i → function.right_inverse (h ∘ f) (g ∘ i)
theorem
function.left_inverse.right_inverse
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.left_inverse g f → function.right_inverse f g
theorem
function.right_inverse.left_inverse
{α : Sort u}
{β : Sort v}
{f : α → β}
{g : β → α} :
function.right_inverse g f → function.left_inverse f g
theorem
function.left_inverse.eq_right_inverse
{α : Sort u}
{β : Sort v}
{f : α → β}
{g₁ g₂ : β → α} :
function.left_inverse g₁ f → function.right_inverse g₂ f → g₁ = g₂
We can use choice to construct explicitly a partial inverse for
a given injective function f.
Equations
- function.partial_inv f b = dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), option.some (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), option.none)
theorem
function.partial_inv_left
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
(I : function.injective f)
(x : α) :
function.partial_inv f (f x) = option.some x
Construct the inverse for a function f on domain s. This function is a right inverse of f
on f '' s.
Equations
- function.inv_fun_on f s b = dite (∃ (a : α), a ∈ s ∧ f a = b) (λ (h : ∃ (a : α), a ∈ s ∧ f a = b), classical.some h) (λ (h : ¬∃ (a : α), a ∈ s ∧ f a = b), classical.choice n)
theorem
function.inv_fun_on_pos
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{s : set α}
{b : β} :
(∃ (a : α) (H : a ∈ s), f a = b) → function.inv_fun_on f s b ∈ s ∧ f (function.inv_fun_on f s b) = b
theorem
function.inv_fun_on_mem
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{s : set α}
{b : β} :
(∃ (a : α) (H : a ∈ s), f a = b) → function.inv_fun_on f s b ∈ s
theorem
function.inv_fun_on_eq
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{s : set α}
{b : β} :
(∃ (a : α) (H : a ∈ s), f a = b) → f (function.inv_fun_on f s b) = b
theorem
function.inv_fun_on_neg
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{s : set α}
{b : β} :
(¬∃ (a : α) (H : a ∈ s), f a = b) → function.inv_fun_on f s b = classical.choice n
The inverse of a function (which is a left inverse if f is injective
and a right inverse if f is surjective).
Equations
theorem
function.inv_fun_eq
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{b : β} :
(∃ (a : α), f a = b) → f (function.inv_fun f b) = b
theorem
function.inv_fun_neg
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{b : β} :
(¬∃ (a : α), f a = b) → function.inv_fun f b = classical.choice n
theorem
function.inv_fun_eq_of_injective_of_right_inverse
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{g : β → α} :
function.injective f → function.right_inverse g f → function.inv_fun f = g
theorem
function.inv_fun_comp
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β} :
function.injective f → function.inv_fun f ∘ f = id
theorem
function.injective.has_left_inverse
{α : Type u}
[i : nonempty α]
{β : Sort v}
{f : α → β} :
theorem
function.injective_iff_has_left_inverse
{α : Type u}
[i : nonempty α]
{β : Sort v}
{f : α → β} :
The inverse of a surjective function. (Unlike inv_fun, this does not require
α to be inhabited.)
Equations
- function.surj_inv h b = classical.some _
theorem
function.surj_inv_eq
{α : Sort u}
{β : Sort v}
{f : α → β}
(h : function.surjective f)
(b : β) :
f (function.surj_inv h b) = b
theorem
function.right_inverse_surj_inv
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.surjective f) :
theorem
function.left_inverse_surj_inv
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.bijective f) :
theorem
function.bijective_iff_has_inverse
{α : Sort u}
{β : Sort v}
{f : α → β} :
function.bijective f ↔ ∃ (g : β → α), function.left_inverse g f ∧ function.right_inverse g f
theorem
function.injective_surj_inv
{α : Sort u}
{β : Sort v}
{f : α → β}
(h : function.surjective f) :
def
function.update
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(f : Π (a : α), β a)
(a' : α)
(v : β a')
(a : α) :
β a
Replacing the value of a function at a given point by a given value.
@[simp]
theorem
function.update_same
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(a : α)
(v : β a)
(f : Π (a : α), β a) :
function.update f a v a = v
@[simp]
theorem
function.update_noteq
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
{a a' : α}
(h : a ≠ a')
(v : β a')
(f : Π (a : α), β a) :
function.update f a' v a = f a
@[simp]
theorem
function.update_eq_self
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(a : α)
(f : Π (a : α), β a) :
function.update f a (f a) = f
theorem
function.update_comp
{α : Sort u}
{α' : Sort w}
[decidable_eq α]
[decidable_eq α']
{β : Sort v}
(f : α → β)
{g : α' → α}
(hg : function.injective g)
(a : α')
(v : β) :
function.update f (g a) v ∘ g = function.update (f ∘ g) a v
theorem
function.comp_update
{α : Sort u}
[decidable_eq α]
{α' : 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_1}
[decidable_eq α]
{β : α → Sort u_2}
{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_1}
[decidable_eq α]
{β : α → Sort u_2}
{a : α}
(v w : β a)
(f : Π (a : α), β a) :
function.update (function.update f a v) a w = function.update f a w
theorem
function.uncurry_def
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ) :
function.uncurry f = λ (p : α × β), f p.fst p.snd
def
function.bicompl
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{ε : Type u_5} :
(γ → δ → ε) → (α → γ) → (β → δ) → α → β → ε
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)
def
function.bicompr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4} :
(γ → δ) → (α → β → γ) → α → β → δ
Compose an unary function f with a binary function g.
Equations
- function.bicompr f g a b = f (g a b)
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
A function is involutive, if f ∘ f = id.
Equations
- function.involutive f = ∀ (x : α), f (f x) = x
The property of a binary function f : α → β → γ being injective.
Mathematically this should be thought of as the corresponding function α × β → γ being injective.
theorem
function.injective2.left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(hf : function.injective2 f)
⦃a₁ a₂ : α⦄
⦃b₁ b₂ : β⦄ :
theorem
function.injective2.right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(hf : function.injective2 f)
⦃a₁ a₂ : α⦄
⦃b₁ b₂ : β⦄ :
theorem
function.injective2.eq_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(hf : function.injective2 f)
⦃a₁ a₂ : α⦄
⦃b₁ b₂ : β⦄ :
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 = dite (nonempty α) (λ (h : nonempty α), f (classical.choice h)) (λ (h : ¬nonempty α), classical.choice _inst_1)
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) :
P (f a) → P (function.sometimes f)