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) :
      eval x f = f x
      theorem Function.const_def {α : Sort u_1} {β : Sort u_2} {y : β} :
      (fun (x : α) => y) = const α y
      theorem Function.const_injective {α : Sort u_1} {β : Sort u_2} [Nonempty α] :
      @[simp]
      theorem Function.const_inj {α : Sort u_1} {β : Sort u_2} [Nonempty α] {y₁ y₂ : β} :
      const α y₁ = const α y₂ y₁ = y₂
      theorem Function.onFun_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : ββγ) (g : αβ) (a b : α) :
      onFun f g a b = f (g a) (g b)
      theorem Function.hfunext {α α' : Sort u} {β : αSort v} {β' : α'Sort v} {f : (a : α) → β a} {f' : (a : α') → β' a} ( : α = α') (h : ∀ (a : α) (a' : α'), a a'f a f' a') :
      f f'
      theorem Function.ne_iff {α : Sort u_1} {β : αSort u_4} {f₁ 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.swap_lt {α : Type u_4} [LT α] :
      (swap fun (x1 x2 : α) => x1 < x2) = fun (x1 x2 : α) => x1 > x2
      theorem Function.swap_le {α : Type u_4} [LE α] :
      (swap fun (x1 x2 : α) => x1 x2) = fun (x1 x2 : α) => x1 x2
      theorem Function.swap_gt {α : Type u_4} [LT α] :
      (swap fun (x1 x2 : α) => x1 > x2) = fun (x1 x2 : α) => x1 < x2
      theorem Function.swap_ge {α : Type u_4} [LE α] :
      (swap fun (x1 x2 : α) => x1 x2) = fun (x1 x2 : α) => x1 x2
      theorem Function.Bijective.injective {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : Bijective f) :
      theorem Function.Bijective.surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : Bijective f) :
      theorem Function.not_injective_iff {α : Sort u_1} {β : Sort u_2} {f : αβ} :
      ¬Injective f (a : α), (b : α), f a = f b a b
      def Function.Injective.decidableEq {α : Sort u_1} {β : Sort u_2} {f : αβ} [DecidableEq β] (I : 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 : Injective (f g)) :
          @[simp]
          theorem Function.Injective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Injective f) (g : γα) :
          theorem Function.Injective.of_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (I : Injective (f g)) (hg : Surjective g) :
          theorem Function.Surjective.bijective₂_of_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : Surjective f) (hg : Surjective g) (I : Injective (f g)) :
          @[simp]
          theorem Function.Injective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) {g : γα} (hg : Bijective g) :
          theorem Function.Injective.piMap {ι : Sort u_4} {α : ιSort u_5} {β : ιSort u_6} {f : (i : ι) → α iβ i} (hf : ∀ (i : ι), Injective (f i)) :
          theorem Function.Injective.comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {g : βγ} (hg : Injective g) :
          Injective fun (x : αβ) => g x

          Composition by an injective function on the left is itself injective.

          theorem Function.injective_comp_left_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [Nonempty α] {g : βγ} :
          (Injective fun (x : αβ) => g x) Injective g
          theorem Function.injective_of_subsingleton {α : Sort u_1} {β : Sort u_2} [Subsingleton α] (f : αβ) :
          theorem Function.bijective_of_subsingleton {α : Sort u_1} [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 : Injective f) (hf' : Injective f') (im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f x, hx f' x', hx') :
          Injective fun (x : α) => if h : p x then f x, h else f' x, h
          theorem Function.Surjective.of_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Surjective (f g)) :
          @[simp]
          theorem Function.Surjective.of_comp_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) {g : γα} (hg : Surjective g) :
          theorem Function.Surjective.of_comp_left {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (S : Surjective (f g)) (hf : Injective f) :
          theorem Function.Injective.bijective₂_of_surjective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : γα} (hf : Injective f) (hg : Injective g) (S : Surjective (f g)) :
          @[simp]
          theorem Function.Surjective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : 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 : Surjective f) {p : βProp} :
            (∀ (y : β), p y) ∀ (x : α), p (f x)
            theorem Function.Surjective.forall₂ {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : 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 : 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 : Surjective f) {p : βProp} :
            ( (y : β), p y) (x : α), p (f x)
            theorem Function.Surjective.exists₂ {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : 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 : 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 : Surjective f) :
            Injective fun (g : βγ) => g f
            theorem Function.injective_comp_right_iff_surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {γ : Type u_4} [Nontrivial γ] :
            (Injective fun (g : βγ) => g f) Surjective f
            theorem Function.Surjective.right_cancellable {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : 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 : αβ) :
            Bijective f ∀ (b : β), ∃! a : α, f a = b
            theorem Function.Bijective.existsUnique {α : Sort u_1} {β : Sort u_2} {f : αβ} (hf : 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 : 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 : Bijective g) :
            theorem Function.Bijective.of_comp_iff' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : 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 : IsPartialInv f g) (x : α) :
                g (f x) = some x
                theorem Function.injective_of_isPartialInv {α : Type u_4} {β : Sort u_5} {f : αβ} {g : βOption α} (H : IsPartialInv f g) :
                theorem Function.injective_of_isPartialInv_right {α : Type u_4} {β : Sort u_5} {f : αβ} {g : βOption α} (H : 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 : 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 : 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 : LeftInverse f g) (hh : LeftInverse h i) :
                LeftInverse (h f) (g i)
                theorem Function.RightInverse.comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : βα} {h : βγ} {i : γβ} (hf : RightInverse f g) (hh : RightInverse h i) :
                RightInverse (h f) (g i)
                theorem Function.LeftInverse.rightInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : LeftInverse g f) :
                theorem Function.RightInverse.leftInverse {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : RightInverse g f) :
                theorem Function.LeftInverse.surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : LeftInverse f g) :
                theorem Function.RightInverse.injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : RightInverse f g) :
                theorem Function.LeftInverse.rightInverse_of_injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : LeftInverse f g) (hf : Injective f) :
                theorem Function.LeftInverse.rightInverse_of_surjective {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : βα} (h : LeftInverse f g) (hg : 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₁ : LeftInverse g₁ f) (h₂ : 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_of_injective {α : Type u_4} {β : Sort u_5} {f : αβ} (I : Injective f) :
                    theorem Function.partialInv_left {α : Type u_4} {β : Sort u_5} {f : αβ} (I : Injective f) (x : α) :
                    partialInv f (f x) = some 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 (invFun f b) = b
                        theorem Function.apply_invFun_apply {α : Type u_3} {β : Type u_4} {f : αβ} {a : α} :
                        f (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 : Injective f) (hg : RightInverse g f) :
                        invFun f = g
                        theorem Function.rightInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Surjective f) :
                        theorem Function.leftInverse_invFun {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Injective f) :
                        theorem Function.invFun_surjective {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Injective f) :
                        theorem Function.invFun_comp {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Injective f) :
                        theorem Function.Injective.hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} (hf : Injective f) :
                        theorem Function.injective_iff_hasLeftInverse {α : Sort u_1} {β : Sort u_2} [Nonempty α] {f : αβ} :
                        noncomputable def Function.surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : 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 : Surjective f) (b : β) :
                            f (surjInv h b) = b
                            theorem Function.rightInverse_surjInv {α : Sort u} {β : Sort v} {f : αβ} (hf : Surjective f) :
                            theorem Function.leftInverse_surjInv {α : Sort u} {β : Sort v} {f : αβ} (hf : Bijective f) :
                            theorem Function.Surjective.hasRightInverse {α : Sort u} {β : Sort v} {f : αβ} (hf : Surjective f) :
                            theorem Function.bijective_iff_has_inverse {α : Sort u} {β : Sort v} {f : αβ} :
                            theorem Function.injective_surjInv {α : Sort u} {β : Sort v} {f : αβ} (h : Surjective f) :
                            theorem Function.surjective_to_subsingleton {α : Sort u} {β : Sort v} [na : Nonempty α] [Subsingleton β] (f : αβ) :
                            theorem Function.Surjective.piMap {ι : Sort u_1} {α : ιSort u_2} {β : ιSort u_3} {f : (i : ι) → α iβ i} (hf : ∀ (i : ι), Surjective (f i)) :
                            theorem Function.Surjective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : Surjective g) :
                            Surjective fun (x : αβ) => g x

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

                            theorem Function.surjective_comp_left_iff {α : Sort u} {β : Sort v} {γ : Sort w} [Nonempty α] {g : βγ} :
                            (Surjective fun (x : αβ) => g x) Surjective g
                            theorem Function.Bijective.piMap {ι : Sort u_1} {α : ιSort u_2} {β : ιSort u_3} {f : (i : ι) → α iβ i} (hf : ∀ (i : ι), Bijective (f i)) :
                            theorem Function.Bijective.comp_left {α : Sort u} {β : Sort v} {γ : Sort w} {g : βγ} (hg : Bijective g) :
                            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_self {α : Sort u} {β : αSort v} [DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a) :
                                update f a v a = v
                                @[deprecated Function.update_self (since := "2024-12-28")]
                                theorem Function.update_same {α : Sort u} {β : αSort v} [DecidableEq α] (a : α) (v : β a) (f : (a : α) → β a) :
                                update f a v a = v

                                Alias of Function.update_self.

                                @[simp]
                                theorem Function.update_of_ne {α : Sort u} {β : αSort v} [DecidableEq α] {a a' : α} (h : a a') (v : β a') (f : (a : α) → β a) :
                                update f a' v a = f a
                                @[deprecated Function.update_of_ne (since := "2024-12-28")]
                                theorem Function.update_noteq {α : Sort u} {β : αSort v} [DecidableEq α] {a a' : α} (h : a a') (v : β a') (f : (a : α) → β a) :
                                update f a' v a = f a

                                Alias of Function.update_of_ne.

                                theorem Function.update_apply {α : Sort u} [DecidableEq α] {β : Sort u_1} (f : αβ) (a' : α) (b : β) (a : α) :
                                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 : αα') :
                                update f a v = const α v
                                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 (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 (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 g : (a : α) → β a} :
                                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 g : (a : α) → β a} :
                                g = 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} :
                                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 = 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 update f a b f a b
                                theorem Function.update_ne_self_iff {α : Sort u} {β : αSort v} [DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a} :
                                update f a b f b f a
                                @[simp]
                                theorem Function.update_eq_self {α : Sort u} {β : αSort v} [DecidableEq α] (a : α) (f : (a : α) → β a) :
                                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 : α') => 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) :
                                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 : Injective f) (i : α') (a : β (f i)) :
                                (fun (j : α') => update g (f i) a (f j)) = update (fun (i : α') => g (f i)) i a
                                theorem Function.update_apply_of_injective {α : Sort u} {β : αSort v} {α' : Sort w} [DecidableEq α] [DecidableEq α'] (g : (a : α) → β a) {f : α'α} (hf : Injective f) (i : α') (a : β (f i)) (j : α') :
                                update g (f i) a (f j) = update (fun (i : α') => g (f i)) i a j
                                theorem Function.update_comp_eq_of_injective {α : Sort u} {α' : Sort w} [DecidableEq α] [DecidableEq α'] {β : Sort u_1} (g : α'β) {f : αα'} (hf : Injective f) (i : α) (a : β) :
                                update g (f i) a f = update (g f) i a

                                Non-dependent version of Function.update_comp_eq_of_injective'

                                theorem Function.rec_update {ι : Sort u_1} {κ : Sort u_2} {α : κSort u_3} [DecidableEq ι] [DecidableEq κ] {ctor : ικ} (hctor : Injective ctor) (recursor : ((i : ι) → α (ctor i))(i : κ) → α i) (h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i) (h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i k)recursor f₁ k = recursor f₂ k) (f : (i : ι) → α (ctor i)) (i : ι) (x : α (ctor i)) :
                                recursor (update f i x) = update (recursor f) (ctor i) x

                                Recursors can be pushed inside Function.update.

                                The ctor argument should be a one-argument constructor like Sum.inl, and recursor should be an inductive recursor partially applied in all but that constructor, such as (Sum.rec · g).

                                In future, we should build some automation to generate applications like Option.rec_update for all inductive types.

                                @[simp]
                                theorem Option.rec_update {α : Type u_1} {β : Option αSort u_2} [DecidableEq α] (f : β none) (g : (a : α) → β (some a)) (a : α) (x : β (some a)) :
                                (fun (t : Option α) => rec f (Function.update g a x) t) = Function.update (fun (t : Option α) => rec f g t) (some a) x
                                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 (update g i v j) = 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 (update g i v j) (update h i w j) = 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 (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 update g i v = 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) :
                                update (update f a v) b w = update (update f b w) a v
                                @[simp]
                                theorem Function.update_idem {α : Sort u_2} [DecidableEq α] {β : αSort u_1} {a : α} (v w : β a) (f : (a : α) → β a) :
                                update (update f a v) a w = update f a w
                                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)] :
                                        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 : Injective f) (g : αγ) :
                                        theorem Function.FactorsThrough.extend_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (hf : FactorsThrough g f) (e' : βγ) (a : α) :
                                        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 : Injective f) (g : αγ) (e' : βγ) (a : α) :
                                        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) :
                                        extend f g e' b = e' b
                                        theorem Function.factorsThrough_iff {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (g : αγ) [Nonempty γ] :
                                        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 (extend f g e' b) = extend f (F g) (F e') b
                                        theorem Function.extend_injective {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Injective f) (e' : βγ) :
                                        Injective fun (g : αγ) => extend f g e'
                                        theorem Function.FactorsThrough.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} {g : αγ} (e' : βγ) (hf : FactorsThrough g f) :
                                        extend f g e' f = g
                                        @[simp]
                                        theorem Function.extend_const {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβ) (c : γ) :
                                        (extend f (fun (x : α) => c) fun (x : β) => c) = fun (x : β) => c
                                        @[simp]
                                        theorem Function.extend_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Injective f) (g : αγ) (e' : βγ) :
                                        extend f g e' f = g
                                        theorem Function.Injective.surjective_comp_right' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Injective f) (g₀ : βγ) :
                                        Surjective fun (g : βγ) => g f
                                        theorem Function.Injective.surjective_comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} [Nonempty γ] (hf : Injective f) :
                                        Surjective fun (g : βγ) => g f
                                        theorem Function.surjective_comp_right_iff_injective {α : Sort u_1} {β : Sort u_2} {f : αβ} {γ : Type u_4} [Nontrivial γ] :
                                        (Surjective fun (g : βγ) => g f) Injective f
                                        theorem Function.Bijective.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβ} (hf : Bijective f) :
                                        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 : FactorsThrough g f) (g' : γδ) :
                                        theorem Function.FactorsThrough.comp_right {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : αβ} {g : αγ} (h : FactorsThrough g f) (g' : δα) :
                                        FactorsThrough (g g') (f g')
                                        theorem Function.uncurry_def {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αβγ) :
                                        uncurry f = fun (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
                                          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} :
                                                      HasUncurry (αβ) α β
                                                      Equations
                                                        instance Function.hasUncurryInduction {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [HasUncurry β γ δ] :
                                                        HasUncurry (αβ) (α × γ) δ
                                                        Equations
                                                          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 : Involutive f) :
                                                              f f = id
                                                              theorem Function.Involutive.leftInverse {α : Sort u} {f : αα} (h : Involutive f) :
                                                              theorem Function.Involutive.leftInverse_iff {α : Sort u} {f : αα} (h : Involutive f) {g : αα} :
                                                              LeftInverse g f g = f
                                                              theorem Function.Involutive.rightInverse {α : Sort u} {f : αα} (h : Involutive f) :
                                                              theorem Function.Involutive.injective {α : Sort u} {f : αα} (h : Involutive f) :
                                                              theorem Function.Involutive.surjective {α : Sort u} {f : αα} (h : Involutive f) :
                                                              theorem Function.Involutive.bijective {α : Sort u} {f : αα} (h : Involutive f) :
                                                              theorem Function.Involutive.ite_not {α : Sort u} {f : αα} (h : 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 : 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 (x1 x2 : α) => f x1 = x2) 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 : Injective2 f) (b : β) :
                                                                  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 : Injective2 f) (a : α) :
                                                                  Injective (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 : Injective2 f) :
                                                                  theorem Function.Injective2.left' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : αβγ} (hf : 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 : Injective2 f) [Nonempty α] :
                                                                  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 : 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) :
                                                                      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 (sometimes f)
                                                                      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 (x1 : α) (x2 : β) => f x1 = x2

                                                                      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 (x1 x2 : α) => f x1 = x2

                                                                      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 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_3} {a a' : α} (h : a = a') :
                                                                          Function.Bijective fun (x : C a) => h x
                                                                          theorem eq_mp_bijective {α β : Sort u_3} (h : α = β) :
                                                                          theorem eq_mpr_bijective {α β : Sort u_3} (h : α = β) :
                                                                          theorem cast_bijective {α β : Sort u_3} (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_3} (x y : C a) :
                                                                          h x = h y x = y
                                                                          @[simp]
                                                                          theorem cast_inj {α β : 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 : 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 : 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 : LeftInverse g f) (C : (a : α) → γ (f a)) (a : α) :
                                                                          cast (C (g (f a))) = C a
                                                                          def Set.SeparatesPoints {α : Type u_3} {β : Type u_4} (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 InvImage.equivalence {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : Equivalence r) :
                                                                              instance instDecidableUncurryOfFstSnd_mathlib {α : Type u_3} {β : Type u_4} {r : αβProp} {x : α × β} [Decidable (r x.fst x.snd)] :
                                                                              Equations
                                                                                instance instDecidableCurryOfMk_mathlib {α : Type u_3} {β : Type u_4} {r : α × βProp} {a : α} {b : β} [Decidable (r (a, b))] :
                                                                                Equations