Documentation

Mathlib.Logic.Function.Basic

Miscellaneous function constructions and lemmas #

@[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
Instances For
    theorem Function.eval_apply {α : Sort u_1} {β : αSort u_4} (x : α) (f : (x : α) → β x) :
    theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
    (fun (x : α) => y) = Function.const α y
    @[simp]
    theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [Nonempty α] {y₁ : β} {y₂ : β} :
    Function.const α y₁ = Function.const α y₂ y₁ = y₂
    theorem Function.id_def {α : Sort u_1} :
    id = fun (x : α) => x
    theorem Function.onFun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : ββγ) (g : αβ) (a : α) (b : α) :
    (f on g) a b = f (g a) (g b)
    theorem Function.hfunext {α : Sort u} {α' : Sort u} {β : αSort v} {β' : α'Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a} (hα : α = α') (h : ∀ (a : α) (a' : α'), HEq a a'HEq (f a) (f' a')) :
    HEq f f'
    theorem Function.ne_iff {α : Sort u_1} {β : αSort u_4} {f₁ : (a : α) → β a} {f₂ : (a : α) → β a} :
    f₁ f₂ ∃ (a : α), f₁ a f₂ a
    theorem Function.funext_iff_of_subsingleton {α : Sort u_1} {β : Sort u_2} {f : αβ} [Subsingleton α] {g : αβ} (x : α) (y : α) :
    f x = g y f = g
    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.beq_eq {α : Type u_4} {β : Type u_5} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {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
    theorem Function.not_injective_iff {α : Sort u_1} {β : Sort u_2} {f : αβ} :
    ¬Function.Injective f ∃ (a : α), ∃ (b : α), f a = f b a b
    def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : αβ} [DecidableEq β] (I : Function.Injective f) :

    If the co-domain β of an injective function f : α → β has decidable equality, then the domain α also has decidable equality.

    Equations
    Instances For
      theorem Function.Injective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (I : Function.Injective (f g)) :
      @[simp]
      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_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (I : Function.Injective (f g)) (hg : Function.Surjective g) :
      theorem Function.Surjective.bijective₂_of_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : Function.Surjective f) (hg : Function.Surjective g) (I : Function.Injective (f g)) :
      @[simp]
      theorem Function.Injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) {g : γα} (hg : Function.Bijective g) :
      theorem Function.Injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : βγ} (hg : Function.Injective g) :
      Function.Injective fun (x : αβ) => g x

      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) [DecidablePred 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 { val := x, property := hx } f' { val := x', property := hx' }) :
      Function.Injective fun (x : α) => if h : p x then f { val := x, property := h } else f' { val := x, property := h }
      theorem Function.Surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Function.Surjective (f g)) :
      @[simp]
      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_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Function.Surjective (f g)) (hf : Function.Injective f) :
      theorem Function.Injective.bijective₂_of_surjective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : Function.Injective f) (hg : Function.Injective g) (S : Function.Surjective (f g)) :
      @[simp]
      theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Bijective f) (g : γα) :
      instance Function.decidableEqPFun (p : Prop) [Decidable p] (α : pType u_4) [(hp : p) → DecidableEq (α hp)] :
      DecidableEq ((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.Surjective.injective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Surjective f) :
      Function.Injective fun (g : βγ) => g f
      theorem Function.Surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Surjective f) {g₁ : βγ} {g₂ : βγ} :
      g₁ f = g₂ f g₁ = g₂
      theorem Function.surjective_of_right_cancellable_Prop {α : Sort u_1} {β : Sort u_2} {f : αβ} (h : ∀ (g₁ g₂ : βProp), g₁ f = g₂ fg₁ = g₂) :
      theorem Function.bijective_iff_existsUnique {α : Sort u_1} {β : Sort u_2} (f : αβ) :
      Function.Bijective f ∀ (b : β), ∃! a : α, f a = b
      theorem Function.Bijective.existsUnique {α : 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_existsUnique.

      theorem Function.Bijective.existsUnique_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) :
      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_4} (f : αSet α) :

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

      theorem Function.cantor_injective {α : Type u_4} (f : Set αα) :

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

      theorem Function.not_surjective_Type {α : Type u} (f : αType (max u v)) :

      There is no surjection from α : Type u into Type (max u v). This theorem demonstrates why Type : Type would be inconsistent in Lean.

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

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

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

        Equations
        Instances For
          theorem Function.partialInv_left {α : Type u_4} {β : Sort u_5} {f : αβ} (I : Function.Injective f) (x : α) :
          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
          Instances For
            theorem Function.invFun_eq {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} {b : β} (h : ∃ (a : α), f a = b) :
            f (Function.invFun f b) = b
            theorem Function.apply_invFun_apply {α : Type u₁} {β : Type u₂} {f : αβ} {a : α} :
            f (Function.invFun f (f a)) = f a
            theorem Function.invFun_neg {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} {b : β} (h : ¬∃ (a : α), f a = b) :
            theorem Function.invFun_eq_of_injective_of_rightInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} {g : βα} (hf : Function.Injective f) (hg : Function.RightInverse g f) :
            theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Function.Surjective f) :
            theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Function.Injective f) :
            theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Function.Injective f) :
            theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Function.Injective f) :
            theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Function.Injective f) :
            noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : Function.Surjective f) (b : β) :
            α

            The inverse of a surjective function. (Unlike invFun, this does not require α to be inhabited.)

            Equations
            Instances For
              theorem Function.surjInv_eq {α : Sort u} {β : Sort v} {f : αβ} (h : Function.Surjective f) (b : β) :
              theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : αβ} (hf : Function.Bijective f) :
              theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {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) :
              Function.Surjective fun (x : αβ) => g x

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

              theorem Function.Bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : Function.Bijective g) :
              Function.Bijective fun (x : αβ) => g x

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

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

                theorem Function.update_eq_const_of_subsingleton {α : Sort u} {α' : Sort w} [DecidableEq α] [Subsingleton α] (a : α) (v : α') (f : αα') :
                theorem Function.surjective_eval {α : Sort u} {β : αSort v} [h : ∀ (a : α), Nonempty (β a)] (a : α) :
                theorem Function.update_injective {α : Sort u} {β : αSort v} [DecidableEq α] (f : (a : α) → β a) (a' : α) :
                theorem Function.forall_update_iff {α : Sort u} {β : αSort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β aProp) :
                (∀ (x : α), p x (Function.update f a b x)) p a b ∀ (x : α), x ap x (f x)
                theorem Function.exists_update_iff {α : Sort u} {β : αSort v} [DecidableEq α] (f : (a : α) → β a) {a : α} {b : β a} (p : (a : α) → β aProp) :
                (∃ (x : α), p x (Function.update f a b x)) p a b ∃ (x : α), x a p x (f x)
                theorem Function.update_eq_iff {α : Sort u} {β : αSort v} [DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {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} [DecidableEq α] {a : α} {b : β a} {f : (a : α) → β a} {g : (a : α) → β a} :
                g = Function.update f a b g a = b ∀ (x : α), x ag x = f x
                @[simp]
                theorem Function.update_eq_self_iff {α : Sort u} {β : αSort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
                Function.update f a b = f b = f a
                @[simp]
                theorem Function.eq_update_self_iff {α : Sort u} {β : αSort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
                f = Function.update f a b f a = b
                theorem Function.ne_update_self_iff {α : Sort u} {β : αSort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
                f Function.update f a b f a b
                theorem Function.update_ne_self_iff {α : Sort u} {β : αSort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
                Function.update f a b f b f a
                @[simp]
                theorem Function.update_eq_self {α : Sort u} {β : αSort v} [DecidableEq α] (a : α) (f : (a : α) → β a) :
                Function.update f a (f a) = f
                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 : α') => Function.update g i a (f j)) = fun (j : α') => g (f j)
                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) :
                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} [DecidableEq α] [DecidableEq α'] (g : (a : α) → β a) {f : α'α} (hf : Function.Injective f) (i : α') (a : β (f i)) :
                (fun (j : α') => Function.update g (f i) a (f j)) = Function.update (fun (i : α') => g (f i)) i a
                theorem Function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [DecidableEq α] [DecidableEq α'] {β : 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} [DecidableEq ι] {α : ι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 (fun (k : ι) => f k (g k)) i (f i v) j
                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 (Function.update g i v j) (Function.update h i w j) = Function.update (fun (k : ι) => f k (g k) (h k)) i (f i v w) j
                theorem Function.pred_update {α : Sort u} {β : αSort v} [DecidableEq α] (P : a : α⦄ → β aProp) (f : (a : α) → β a) (a' : α) (v : β a') (a : α) :
                P (Function.update f a' v a) a = a' P v a a' P (f a)
                theorem Function.comp_update {α : Sort u} [DecidableEq α] {α' : 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_2} [DecidableEq α] {β : αSort u_1} {a : α} {b : α} (h : a b) (v : β a) (w : β b) (f : (a : α) → β a) :
                @[simp]
                theorem Function.update_idem {α : Sort u_2} [DecidableEq α] {β : αSort u_1} {a : α} (v : β a) (w : β a) (f : (a : α) → β a) :
                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
                Instances For
                  def Function.FactorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (g : αγ) (f : αβ) :

                  g factors through f : f a = f b → g a = g b

                  Equations
                  Instances For
                    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 = if h : ∃ (a : α), f a = b then g (Classical.choose h) else e' b
                    theorem Function.Injective.factorsThrough {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Injective f) (g : αγ) :
                    theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (hf : Function.FactorsThrough g f) (e' : βγ) (a : α) :
                    Function.extend f g e' (f a) = g a
                    @[simp]
                    theorem Function.Injective.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.factorsThrough_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (g : αγ) [Nonempty γ] :
                    Function.FactorsThrough g f ∃ (e : βγ), g = e f
                    theorem Function.apply_extend {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {g : αγ} (F : γδ) (f : αβ) (e' : βγ) (b : β) :
                    F (Function.extend f g e' b) = Function.extend f (F g) (F e') b
                    theorem Function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Injective f) (e' : βγ) :
                    Function.Injective fun (g : αγ) => Function.extend f g e'
                    theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (e' : βγ) (hf : Function.FactorsThrough g f) :
                    Function.extend f g e' f = g
                    @[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 fun (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 fun (g : βγ) => g f
                    theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Function.Bijective f) :
                    Function.Bijective fun (g : βγ) => g f
                    theorem Function.FactorsThrough.rfl {α : Sort u_1} {β : Sort u_2} {f : αβ} :
                    theorem Function.FactorsThrough.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : αβ} {g : αγ} (h : Function.FactorsThrough g f) (g' : γδ) :
                    theorem Function.FactorsThrough.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : αβ} {g : αγ} (h : Function.FactorsThrough g f) (g' : δα) :
                    theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
                    Function.uncurry f = fun (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
                    Instances For
                      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
                      Instances For
                        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 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

                          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
                          Instances For
                            instance Function.hasUncurryBase {α : Type u_1} {β : Type u_2} :
                            Function.HasUncurry (αβ) α β
                            Equations
                            • Function.hasUncurryBase = { uncurry := id }
                            instance Function.hasUncurryInduction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Function.HasUncurry β γ δ] :
                            Function.HasUncurry (αβ) (α × γ) δ
                            Equations
                            • Function.hasUncurryInduction = { uncurry := fun (f : αβ) (p : α × γ) => ((f p.fst)) p.snd }
                            def Function.Involutive {α : Sort u_1} (f : αα) :

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

                            Equations
                            Instances For
                              @[simp]
                              theorem Function.Involutive.comp_self {α : Sort u} {f : αα} (h : Function.Involutive f) :
                              f f = id
                              theorem Function.Involutive.ite_not {α : Sort u} {f : αα} (h : Function.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.

                              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.

                              @[simp]
                              theorem Function.symmetric_apply_eq_iff {α : Sort u_1} {f : αα} :
                              (Symmetric fun (x x_1 : α) => f x = x_1) Function.Involutive f
                              def Function.Injective2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) :

                              The property of a binary function f : α → β → γ being injective. Mathematically this should be thought of as the corresponding function α × β → γ being injective.

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

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

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

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

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

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

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

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

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

                                  theorem forall_existsUnique_iff' {α : Sort u_1} {β : Sort u_2} {r : αβProp} :
                                  (∀ (a : α), ∃! b : β, r a b) ∃ (f : αβ), r = fun (x : α) (x_1 : β) => f x = x_1

                                  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.

                                  theorem Symmetric.forall_existsUnique_iff' {α : Sort u_1} {r : ααProp} (hr : Symmetric r) :
                                  (∀ (a : α), ∃! b : α, r a b) ∃ (f : αα), Function.Involutive f r = fun (x x_1 : α) => f x = x_1

                                  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.

                                  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.

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

                                    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') :
                                    Function.Bijective fun (x : C a) => hx
                                    theorem eq_mp_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :
                                    theorem eq_mpr_bijective {α : Sort u_1} {β : Sort u_1} (h : α = β) :
                                    theorem cast_bijective {α : Sort u_1} {β : 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 : C a) (y : C a) :
                                    hx = hy x = y
                                    @[simp]
                                    theorem cast_inj {α : Type u} {β : Type u} (h : α = β) {x : α} {y : α} :
                                    cast h x = cast h y x = y
                                    theorem Function.LeftInverse.eq_rec_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
                                    C (g (f a)) = C a
                                    theorem Function.LeftInverse.eq_rec_on_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
                                    Eq.recOn (C (g (f a))) = C a
                                    theorem Function.LeftInverse.cast_eq {α : Sort u_1} {β : Sort u_2} {γ : βSort v} {f : αβ} {g : βα} (h : Function.LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
                                    cast (C (g (f a))) = C a
                                    def Set.SeparatesPoints {α : Type u_1} {β : Type u_2} (A : Set (αβ)) :

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

                                    Equations
                                    Instances For
                                      theorem IsSymmOp.flip_eq {α : Sort u_1} {β : Sort u_2} (op : ααβ) [IsSymmOp α β op] :
                                      flip op = op
                                      theorem InvImage.equivalence {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : Equivalence r) :
                                      instance instDecidableUncurryProp {α : Type u_1} {β : Type u_2} {r : αβProp} {x : α × β} [Decidable (r x.fst x.snd)] :
                                      Equations
                                      • instDecidableUncurryProp = inst
                                      instance instDecidableCurryProp {α : Type u_1} {β : Type u_2} {r : α × βProp} {a : α} {b : β} [Decidable (r (a, b))] :
                                      Equations
                                      • instDecidableCurryProp = inst