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_1}
{β : α → Sort u_2}
(x : α)
(f : Π (x : α), β x) :
function.eval x f = f x
theorem
function.comp_apply
{α : Sort u}
{β : Sort v}
{φ : Sort w}
(f : β → φ)
(g : α → β)
(a : α) :
theorem
function.const_def
{α : Sort u_1}
{β : Sort u_2}
{y : β} :
(λ (x : α), y) = function.const α y
@[simp]
theorem
function.const_apply
{α : Sort u_1}
{β : Sort u_2}
{y : β}
{x : α} :
function.const α y x = y
@[simp]
theorem
function.const_comp
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{c : γ} :
function.const β c ∘ f = function.const α c
@[simp]
theorem
function.comp_const
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : β → γ}
{b : β} :
f ∘ function.const α b = function.const α (f b)
@[simp]
theorem
function.injective.eq_iff
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(I : function.injective f)
{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) :
theorem
function.injective.ne
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(hf : function.injective f)
{a₁ 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 : α} :
theorem
function.injective.ne_iff'
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(hf : function.injective f)
{x y : α}
{z : β}
(h : f y = z) :
def
function.injective.decidable_eq
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
[decidable_eq β]
(I : function.injective f) :
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_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{g : γ → α}
(I : function.injective (f ∘ g)) :
theorem
function.surjective.of_comp
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{g : γ → α}
(S : function.surjective (f ∘ g)) :
@[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_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₃)
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.
theorem
function.is_partial_inv_left
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : β → option α}
(H : function.is_partial_inv f g)
(x : α) :
theorem
function.injective_of_partial_inv
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
{g : β → option α}
(H : function.is_partial_inv f g) :
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 : α)
(h₁ : b ∈ g x)
(h₂ : b ∈ g y) :
x = y
theorem
function.left_inverse.comp_eq_id
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g) :
theorem
function.left_inverse_iff_comp
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α} :
function.left_inverse f g ↔ f ∘ g = id
theorem
function.right_inverse.comp_eq_id
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.right_inverse f g) :
theorem
function.right_inverse_iff_comp
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α} :
function.right_inverse f g ↔ g ∘ f = id
theorem
function.left_inverse.comp
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{g : β → α}
{h : β → γ}
{i : γ → β}
(hf : function.left_inverse f g)
(hh : function.left_inverse h i) :
function.left_inverse (h ∘ f) (g ∘ i)
theorem
function.right_inverse.comp
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{g : β → α}
{h : β → γ}
{i : γ → β}
(hf : function.right_inverse f g)
(hh : function.right_inverse h i) :
function.right_inverse (h ∘ f) (g ∘ i)
theorem
function.left_inverse.right_inverse
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.left_inverse g f) :
theorem
function.right_inverse.left_inverse
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.right_inverse g f) :
theorem
function.left_inverse.surjective
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g) :
theorem
function.right_inverse.injective
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.right_inverse f g) :
theorem
function.left_inverse.eq_right_inverse
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g₁ g₂ : β → α}
(h₁ : function.left_inverse g₁ f)
(h₂ : 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), some (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), none)
theorem
function.partial_inv_of_injective
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
(I : function.injective f) :
theorem
function.partial_inv_left
{α : Type u_1}
{β : Sort u_2}
{f : α → β}
(I : function.injective f)
(x : α) :
function.partial_inv f (f x) = some x
def
function.inv_fun_on
{α : Type u}
[n : nonempty α]
{β : Sort v}
(f : α → β)
(s : set α)
(b : β) :
α
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 : β}
(h : ∃ (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 : β}
(h : ∃ (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 : β}
(h : ∃ (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 : β}
(h : ¬∃ (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 : β}
(h : ∃ (a : α), f a = b) :
f (function.inv_fun f b) = b
theorem
function.inv_fun_neg
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{b : β}
(h : ¬∃ (a : α), f a = b) :
theorem
function.inv_fun_eq_of_injective_of_right_inverse
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
{g : β → α}
(hf : function.injective f)
(hg : function.right_inverse g f) :
function.inv_fun f = g
theorem
function.right_inverse_inv_fun
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
(hf : function.surjective f) :
theorem
function.left_inverse_inv_fun
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
(hf : function.injective f) :
theorem
function.inv_fun_surjective
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
(hf : function.injective f) :
theorem
function.inv_fun_comp
{α : Type u}
[n : nonempty α]
{β : Sort v}
{f : α → β}
(hf : function.injective f) :
function.inv_fun f ∘ f = id
theorem
function.injective.has_left_inverse
{α : Type u}
[i : nonempty α]
{β : Sort v}
{f : α → β}
(hf : function.injective 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.surjective.has_right_inverse
{α : Sort u}
{β : Sort v}
{f : α → β}
(hf : function.surjective 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
def
function.extend
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : α → γ)
(e' : β → γ)
(a : β) :
γ
extend f g e' extends a function g : α → γ
along a function f : α → β to a function β → γ,
by using the values of g on the range of f
and the values of an auxiliary function e' : β → γ elsewhere.
Mostly useful when f is injective.
Equations
- function.extend f g e' = λ (b : β), dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), g (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), e' b)
theorem
function.extend_def
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : α → γ)
(e' : β → γ)
(b : β) :
function.extend f g e' b = dite (∃ (a : α), f a = b) (λ (h : ∃ (a : α), f a = b), g (classical.some h)) (λ (h : ¬∃ (a : α), f a = b), e' b)
@[simp]
theorem
function.extend_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
(hf : function.injective f)
(g : α → γ)
(e' : β → γ)
(a : α) :
function.extend f g e' (f a) = g a
@[simp]
theorem
function.extend_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
(hf : function.injective f)
(g : α → γ)
(e' : β → γ) :
function.extend f g e' ∘ f = g
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}
(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)
def
function.bicompr
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
(f : γ → δ)
(g : α → β → γ)
(a : α)
(b : β) :
δ
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
@[class]
structure
function.has_uncurry
(α : Type u_5)
(β : out_param (Type u_6))
(γ : out_param (Type u_7)) :
Type (max u_5 u_6 u_7)
- uncurry : α → β → γ
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.
@[instance]
Equations
- function.has_uncurry_base = {uncurry := id (α → β)}
@[instance]
def
function.has_uncurry_induction
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[function.has_uncurry β γ δ] :
function.has_uncurry (α → β) (α × γ) δ
A function is involutive, if f ∘ f = id.
Equations
- function.involutive f = ∀ (x : α), f (f x) = x
@[simp]
theorem
function.involutive.ite_not
{α : Sort u}
{f : α → α}
(h : function.involutive f)
(P : Prop)
[decidable P]
(x : α) :
Involuting an ite of an involuted value x : α negates the Prop condition in the ite.
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₂ : β⦄
(h : f a₁ b₁ = f a₂ b₂) :
a₁ = a₂
theorem
function.injective2.right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(hf : function.injective2 f)
⦃a₁ a₂ : α⦄
⦃b₁ b₂ : β⦄
(h : f a₁ b₁ = f a₂ b₂) :
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)
(h : P (f a)) :
P (function.sometimes f)