mathlib documentation

logic.function.basic

Miscellaneous function constructions and lemmas #

def function.eval {α : Sort u_1} {β : α → Sort u_2} (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
@[simp]
theorem function.eval_apply {α : Sort u_1} {β : α → Sort u_2} (x : α) (f : Π (x : α), β x) :
theorem function.comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g : α → β) (a : α) :
(f g) a = 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 : γ} :
@[simp]
theorem function.comp_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : β → γ} {b : β} :
theorem function.id_def {α : Sort u_1} :
id = λ (x : α), x
@[ext]
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'
theorem function.funext_iff {α : Sort u_1} {β : α → Sort u_2} {f₁ f₂ : Π (x : α), β x} :
f₁ = f₂ ∀ (a : α), f₁ a = f₂ a
theorem function.bijective.injective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) :
theorem function.bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.bijective f) :
theorem function.injective.eq_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) {a b : α} :
f a = f b a = b
theorem function.injective.eq_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (I : function.injective f) {a b : α} {c : β} (h : f b = c) :
f a = c a = b
theorem function.injective.ne {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.injective f) {a₁ a₂ : α} :
a₁ a₂f a₁ f a₂
theorem function.injective.ne_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.injective f) {x y : α} :
f x f y x y
theorem function.injective.ne_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.injective f) {x y : α} {z : β} (h : f y = z) :
f x z x y
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
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 : γ → α) :
theorem function.injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : function.bijective g) :
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) :
theorem function.surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.bijective 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
theorem function.surjective.forall {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∀ (y : β), p y) ∀ (x : α), p (f x)
theorem function.surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → Prop} :
(∀ (y₁ y₂ : β), p y₁ y₂) ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
theorem function.surjective.forall₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → β → Prop} :
(∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
theorem function.surjective.exists {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → Prop} :
(∃ (y : β), p y) ∃ (x : α), p (f x)
theorem function.surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → Prop} :
(∃ (y₁ y₂ : β), p y₁ y₂) ∃ (x₁ x₂ : α), p (f x₁) (f x₂)
theorem function.surjective.exists₃ {α : Sort u_1} {β : Sort u_2} {f : α → β} (hf : function.surjective f) {p : β → β → β → Prop} :
(∃ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ∃ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
theorem function.bijective_iff_exists_unique {α : Sort u_1} {β : Sort u_2} (f : α → β) :
function.bijective f ∀ (b : β), ∃! (a : α), f a = b
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.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α} (hg : function.bijective g) :
theorem function.bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (hf : function.bijective f) (g : γ → α) :
theorem function.cantor_surjective {α : Type u_1} (f : α → set α) :

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

theorem function.cantor_injective {α : Type u_1} (f : set α → α) :

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

def function.is_partial_inv {α : Type u_1} {β : Sort u_2} (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
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) = some 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) :
f g = id
theorem function.left_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
theorem function.right_inverse.comp_eq_id {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} (h : function.right_inverse f g) :
g f = id
theorem function.right_inverse_iff_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α} :
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) :
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) :
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₂
def function.partial_inv {α : Type u_1} {β : Sort u_2} (f : α → β) (b : β) :

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

Equations
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 : α) :
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
theorem function.inv_fun_on_pos {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} (h : ∃ (a : α) (H : a s), f a = 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) :
theorem function.inv_fun_on_eq {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} (h : ∃ (a : α) (H : a s), f a = b) :
theorem function.inv_fun_on_eq' {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {a : α} (h : ∀ (x : α), x s∀ (y : α), y sf x = f yx = y) (ha : a s) :
theorem function.inv_fun_on_neg {α : Type u} [n : nonempty α] {β : Sort v} {f : α → β} {s : set α} {b : β} (h : ¬∃ (a : α) (H : a s), f a = b) :
def function.inv_fun {α : Type u} [n : nonempty α] {β : Sort v} (f : α → β) :
β → α

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) :
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) :
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) :
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 : α → β} :
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
theorem function.surj_inv_eq {α : Sort u} {β : Sort v} {f : α → β} (h : function.surjective f) (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.surjective_iff_has_right_inverse {α : Sort u} {β : Sort v} {f : α → β} :
theorem function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {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 : α → β) :
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.

Equations
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 ap x (f x)
theorem function.update_eq_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] {a : α} {b : β a} {f g : Π (a : α), β a} :
function.update f a b = g b = g a ∀ (x : α), x af x = g x
theorem function.eq_update_iff {α : Sort u} {β : α → Sort v} [decidable_eq α] {a : α} {b : β a} {f g : Π (a : α), β a} :
g = function.update f a b g a = b ∀ (x : α), x ag x = f x
@[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.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) :
@[simp]
theorem function.update_idem {α : Sort u_1} [decidable_eq α] {β : α → Sort u_2} {a : α} (v w : β a) (f : Π (a : α), β a) :
def function.extend {α : Type u_1} {β : Type u_2} {γ : Type 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
theorem function.extend_def {α : Type u_1} {β : Type u_2} {γ : Type 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 {α : 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_apply' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ (a : α), f a = b) :
function.extend f g e' b = e' b
theorem function.extend_injective {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} (hf : function.injective f) (e' : β → γ) :
function.injective (λ (g : α → γ), function.extend f g e')
@[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
@[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
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
theorem function.uncurry_bicompr {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ) (g : γ → δ) :
theorem function.uncurry_bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : γ → δ → ε) (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.

Instances
@[instance]
def function.has_uncurry_base {α : Type u_1} {β : Type u_2} :
function.has_uncurry (α → β) α β
Equations
@[instance]
def function.has_uncurry_induction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [function.has_uncurry β γ δ] :
function.has_uncurry (α → β) × γ) δ
Equations
def function.involutive {α : Sort u_1} (f : α → α) :
Prop

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

Equations
theorem function.involutive_iff_iter_2_eq_id {α : Sort u_1} {f : α → α} :
@[simp]
theorem function.involutive.comp_self {α : Sort u} {f : α → α} (h : function.involutive f) :
f f = id
theorem function.involutive.left_inverse {α : Sort u} {f : α → α} (h : function.involutive f) :
theorem function.involutive.right_inverse {α : Sort u} {f : α → α} (h : function.involutive f) :
theorem function.involutive.injective {α : Sort u} {f : α → α} (h : function.involutive f) :
theorem function.involutive.surjective {α : Sort u} {f : α → α} (h : function.involutive f) :
theorem function.involutive.bijective {α : Sort u} {f : α → α} (h : function.involutive f) :
theorem function.involutive.ite_not {α : Sort u} {f : α → α} (h : function.involutive f) (P : Prop) [decidable P] (x : α) :
f (ite P x (f x)) = ite (¬P) x (f x)

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

theorem function.involutive.eq_iff {α : Sort u} {f : α → α} (h : function.involutive f) {x y : α} :
f x = y x = f y

An involution commutes across an equality. Compare to function.injective.eq_iff.

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₂
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₂ : β⦄ :
f a₁ b₁ = f a₂ b₂ a₁ = a₂ b₁ = b₂
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
theorem function.sometimes_eq {p : Prop} {α : Sort u_1} [nonempty α] (f : p → α) (a : p) :
theorem function.sometimes_spec {p : Prop} {α : Sort u_1} [nonempty α] (P : α → Prop) (f : p → α) (a : p) (h : P (f a)) :
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

Bijectivity of eq.rec, eq.mp, eq.mpr, and cast #

theorem eq_rec_on_bijective {α : Sort u_1} {C : α → Sort u_2} {a a' : α} (h : a = a') :
theorem eq_mp_bijective {α β : Sort u_1} (h : α = β) :
theorem eq_mpr_bijective {α β : Sort u_1} (h : α = β) :
theorem cast_bijective {α β : Sort u_1} (h : α = β) :

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

@[simp]
theorem eq_rec_inj {α : Sort u_1} {a a' : α} (h : a = a') {C : α → Type u_2} (x y : C a) :
eq.rec x h = eq.rec y h x = y
@[simp]
theorem cast_inj {α β : Type u_1} (h : α = β) {x y : α} :
cast h x = cast h y x = y
def set.separates_points {α : Type u_1} {β : Type u_2} (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
theorem is_symm_op.flip_eq {α : Type u_1} {β : out_param (Type u_2)} (op : α → α → β) [is_symm_op α β op] :
flip op = op