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)
@[protected]
theorem
function.bijective.injective
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(hf : function.bijective f) :
@[protected]
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 : α} :
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₂ : α} :
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.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_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.comp_left
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{g : β → γ}
(hg : function.injective g) :
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)
[decidable_pred 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 (λ (x : α), dite (p x) (λ (h : p x), f ⟨x, h⟩) (λ (h : ¬p x), f' ⟨x, h⟩))
theorem
function.surjective.of_comp
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
{g : γ → α}
(S : function.surjective (f ∘ g)) :
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_iff'
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
(hf : function.bijective f)
(g : γ → α) :
function.surjective (f ∘ g) ↔ function.surjective g
@[protected, 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) _
@[protected]
theorem
function.surjective.forall
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(hf : function.surjective f)
{p : β → Prop} :
(∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
@[protected]
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₂)
@[protected]
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₃)
@[protected]
theorem
function.surjective.exists
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
(hf : function.surjective f)
{p : β → Prop} :
(∃ (y : β), p y) ↔ ∃ (x : α), p (f x)
@[protected]
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₂)
@[protected]
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 (λ (g : β → γ), g ∘ f)
@[protected]
theorem
function.surjective.right_cancellable
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
(hf : function.surjective 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_exists_unique
{α : Sort u_1}
{β : Sort u_2}
(f : α → β) :
function.bijective f ↔ ∀ (b : β), ∃! (a : α), f a = b
@[protected]
theorem
function.bijective.exists_unique
{α : 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_exists_unique.
theorem
function.bijective.exists_unique_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
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.right_inverse_of_injective
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g)
(hf : function.injective f) :
theorem
function.left_inverse.right_inverse_of_surjective
{α : Sort u_1}
{β : Sort u_2}
{f : α → β}
{g : β → α}
(h : function.left_inverse f g)
(hg : function.surjective 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
noncomputable
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. For a computable version, see function.injective.inv_of_mem_range.
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
- function.inv_fun f = λ (y : β), dite (∃ (x : α), f x = y) (λ (h : ∃ (x : α), f x = y), h.some) (λ (h : ¬∃ (x : α), f x = y), classical.arbitrary α)
theorem
function.inv_fun_eq
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
{b : β}
(h : ∃ (a : α), f a = b) :
f (function.inv_fun f b) = b
theorem
function.inv_fun_neg
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
{b : β}
(h : ¬∃ (a : α), f a = b) :
function.inv_fun f b = classical.choice _inst_1
theorem
function.inv_fun_eq_of_injective_of_right_inverse
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
{g : β → α}
(hf : function.injective f)
(hg : function.right_inverse g f) :
function.inv_fun f = g
theorem
function.right_inverse_inv_fun
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
(hf : function.surjective f) :
theorem
function.left_inverse_inv_fun
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
(hf : function.injective f) :
theorem
function.inv_fun_surjective
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
(hf : function.injective f) :
theorem
function.inv_fun_comp
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
(hf : function.injective f) :
function.inv_fun f ∘ f = id
theorem
function.injective.has_left_inverse
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β}
(hf : function.injective f) :
theorem
function.injective_iff_has_left_inverse
{α : Sort u_1}
{β : Sort u_2}
[nonempty α]
{f : α → β} :
noncomputable
def
function.surj_inv
{α : Sort u}
{β : Sort v}
{f : α → β}
(h : function.surjective f)
(b : β) :
α
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) :
theorem
function.surjective_to_subsingleton
{α : Sort u}
{β : Sort v}
[na : nonempty α]
[subsingleton β]
(f : α → β) :
theorem
function.surjective.comp_left
{α : Sort u}
{β : Sort v}
{γ : Sort w}
{g : β → γ}
(hg : function.surjective g) :
Composition by an surjective function on the left is itself surjective.
theorem
function.bijective.comp_left
{α : Sort u}
{β : Sort v}
{γ : Sort w}
{g : β → γ}
(hg : function.bijective g) :
Composition by an bijective function on the left is itself bijective.
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.
theorem
function.update_apply
{α : Sort u}
[decidable_eq α]
{β : Sort u_1}
(f : α → β)
(a' : α)
(b : β)
(a : α) :
function.update f a' b a = ite (a = a') b (f a)
On non-dependent functions, function.update can be expressed as an ite
@[simp]
theorem
function.update_same
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(a : α)
(v : β a)
(f : Π (a : α), β a) :
function.update f a v a = v
theorem
function.surjective_eval
{α : Sort u}
{β : α → Sort v}
[h : ∀ (a : α), nonempty (β a)]
(a : α) :
theorem
function.update_injective
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(f : Π (a : α), β a)
(a' : α) :
@[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
theorem
function.forall_update_iff
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
(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}
[decidable_eq α]
(f : Π (a : α), β a)
{a : α}
{b : β a}
(p : Π (a : α), β a → Prop) :
(∃ (x : α), p x (function.update f a b x)) ↔ p a b ∨ ∃ (x : α) (H : x ≠ a), p x (f x)
theorem
function.update_eq_iff
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
{a : α}
{b : β a}
{f g : Π (a : α), β a} :
theorem
function.eq_update_iff
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
{a : α}
{b : β a}
{f g : Π (a : α), β 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_eq_of_forall_ne'
{α : Sort u}
{β : α → Sort v}
[decidable_eq α]
{α' : Sort u_1}
(g : Π (a : α), β a)
{f : α' → α}
{i : α}
(a : β i)
(h : ∀ (x : α'), f x ≠ i) :
(λ (j : α'), function.update g i a (f j)) = λ (j : α'), g (f j)
theorem
function.update_comp_eq_of_forall_ne
{α' : Sort w}
[decidable_eq α']
{α : 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}
[decidable_eq α]
[decidable_eq α']
(g : Π (a : α), β a)
{f : α' → α}
(hf : function.injective f)
(i : α')
(a : β (f i)) :
(λ (j : α'), function.update g (f i) a (f j)) = function.update (λ (i : α'), g (f i)) i a
theorem
function.update_comp_eq_of_injective
{α : Sort u}
{α' : Sort w}
[decidable_eq α]
[decidable_eq α']
{β : 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}
[decidable_eq ι]
{α : ι → 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 (λ (k : ι), f k (g k)) i (f i v) j
theorem
function.apply_update₂
{ι : Sort u_1}
[decidable_eq ι]
{α : ι → 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 (λ (k : ι), f k (g k) (h k)) i (f i v w) j
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
noncomputable
def
function.extend
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
(f : α → β)
(g : α → γ)
(e' : β → γ) :
β → γ
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
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
(f : α → β)
(g : α → γ)
(e' : β → γ)
(b : β)
[decidable (∃ (a : α), f a = 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
{α : 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.extend_injective
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
(hf : function.injective f)
(e' : β → γ) :
function.injective (λ (g : α → γ), function.extend f g e')
@[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 (λ (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 (λ (g : β → γ), g ∘ f)
theorem
function.bijective.comp_right
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
{f : α → β}
(hf : function.bijective f) :
function.bijective (λ (g : β → γ), g ∘ f)
theorem
function.uncurry_def
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ) :
function.uncurry f = λ (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)
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.
@[protected, instance]
Equations
- function.has_uncurry_base = {uncurry := id (α → β)}
@[protected, 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]
@[protected]
@[protected]
@[protected]
@[protected]
@[protected]
@[protected]
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.
@[protected]
An involution commutes across an equality. Compare to function.injective.eq_iff.
The property of a binary function f : α → β → γ being injective.
Mathematically this should be thought of as the corresponding function α × β → γ being injective.
@[protected]
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₂
@[protected]
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)
theorem
eq_rec_on_bijective
{α : Sort u_1}
{C : α → Sort u_2}
{a a' : α}
(h : a = a') :
function.bijective h.rec_on
Note these lemmas apply to Type* not Sort*, as the latter interferes with simp, and
is trivial anyway.
A set of functions "separates points" if for each pair of distinct points there is a function taking different values on them.
Equations
- A.separates_points = ∀ ⦃x y : α⦄, x ≠ y → (∃ (f : α → β) (H : f ∈ A), f x ≠ f y)
theorem
is_symm_op.flip_eq
{α : Type u_1}
{β : out_param (Type u_2)}
(op : α → α → β)
[is_symm_op α β op] :