Documentation

Mathlib.Logic.Function.Defs

General operations on functions #

theorem Function.flip_def {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {f : αβφ} :
flip f = fun (b : β) (a : α) => f a b
@[reducible, inline]
def Function.dcomp {α : Sort u₁} {β : αSort u₂} {φ : {x : α} → β xSort u₃} (f : {x : α} → (y : β x) → φ y) (g : (x : α) → β x) (x : α) :
φ (g x)

Composition of dependent functions: (f ∘' g) x = f (g x), where type of g x depends on x and type of f (g x) depends on x and g x.

Equations
Instances For
    @[reducible, deprecated]
    def Function.compRight {α : Sort u₁} {β : Sort u₂} (f : βββ) (g : αβ) :
    βαβ
    Equations
    Instances For
      @[reducible, deprecated]
      def Function.compLeft {α : Sort u₁} {β : Sort u₂} (f : βββ) (g : αβ) :
      αββ
      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.onFun {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : ββφ) (g : αβ) :
        ααφ

        Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. Can be used, e.g., to transfer a relation from β to α.

        Equations
        • (f on g) x y = f (g x) (g y)
        Instances For

          Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. Can be used, e.g., to transfer a relation from β to α.

          Equations
          Instances For
            @[reducible, deprecated]
            def Function.combine {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₅} (f : αβφ) (op : φδζ) (g : αβδ) :
            αβζ

            Given functions f : α → β → φ, g : α → β → δ and a binary operator op : φ → δ → ζ, produce a function α → β → ζ that applies f and g on each argument and then applies op to the results.

            Equations
            Instances For
              @[reducible, inline]
              abbrev Function.swap {α : Sort u₁} {β : Sort u₂} {φ : αβSort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
              φ x y
              Equations
              Instances For
                theorem Function.swap_def {α : Sort u₁} {β : Sort u₂} {φ : αβSort u₃} (f : (x : α) → (y : β) → φ x y) :
                Function.swap f = fun (y : β) (x : α) => f x y
                @[reducible, deprecated]
                def Function.app {α : Sort u₁} {β : αSort u₂} (f : (x : α) → β x) (x : α) :
                β x
                Equations
                Instances For
                  @[simp]
                  theorem Function.id_comp {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  id f = f
                  @[deprecated Function.id_comp]
                  theorem Function.left_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  id f = f

                  Alias of Function.id_comp.

                  @[deprecated Function.id_comp]
                  theorem Function.comp.left_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  id f = f

                  Alias of Function.id_comp.

                  @[simp]
                  theorem Function.comp_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  f id = f
                  @[deprecated Function.comp_id]
                  theorem Function.right_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  f id = f

                  Alias of Function.comp_id.

                  @[deprecated Function.comp_id]
                  theorem Function.comp.right_id {α : Sort u₁} {β : Sort u₂} (f : αβ) :
                  f id = f

                  Alias of Function.comp_id.

                  theorem Function.comp_assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φδ) (g : βφ) (h : αβ) :
                  (f g) h = f g h
                  @[deprecated Function.comp_assoc]
                  theorem Function.comp.assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φδ) (g : βφ) (h : αβ) :
                  (f g) h = f g h

                  Alias of Function.comp_assoc.

                  @[deprecated Function.comp_const]
                  theorem Function.comp_const_right {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} {f : βγ} {b : β} :

                  Alias of Function.comp_const.

                  def Function.Injective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

                  A function f : α → β is called injective if f x = f y implies x = y.

                  Equations
                  Instances For
                    theorem Function.Injective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} (hg : Function.Injective g) (hf : Function.Injective f) :
                    def Function.Surjective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

                    A function f : α → β is called surjective if every b : β is equal to f a for some a : α.

                    Equations
                    Instances For
                      theorem Function.Surjective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} (hg : Function.Surjective g) (hf : Function.Surjective f) :
                      def Function.Bijective {α : Sort u₁} {β : Sort u₂} (f : αβ) :

                      A function is called bijective if it is both injective and surjective.

                      Equations
                      Instances For
                        theorem Function.Bijective.comp {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {g : βφ} {f : αβ} :
                        def Function.LeftInverse {α : Sort u₁} {β : Sort u₂} (g : βα) (f : αβ) :

                        LeftInverse g f means that g is a left inverse to f. That is, g ∘ f = id.

                        Equations
                        Instances For
                          def Function.HasLeftInverse {α : Sort u₁} {β : Sort u₂} (f : αβ) :

                          HasLeftInverse f means that f has an unspecified left inverse.

                          Equations
                          Instances For
                            def Function.RightInverse {α : Sort u₁} {β : Sort u₂} (g : βα) (f : αβ) :

                            RightInverse g f means that g is a right inverse to f. That is, f ∘ g = id.

                            Equations
                            Instances For
                              def Function.HasRightInverse {α : Sort u₁} {β : Sort u₂} (f : αβ) :

                              HasRightInverse f means that f has an unspecified right inverse.

                              Equations
                              Instances For
                                theorem Function.LeftInverse.injective {α : Sort u₁} {β : Sort u₂} {g : βα} {f : αβ} :
                                theorem Function.HasLeftInverse.injective {α : Sort u₁} {β : Sort u₂} {f : αβ} :
                                theorem Function.rightInverse_of_injective_of_leftInverse {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (injf : Function.Injective f) (lfg : Function.LeftInverse f g) :
                                theorem Function.RightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (h : Function.RightInverse g f) :
                                theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (surjf : Function.Surjective f) (rfg : Function.RightInverse f g) :
                                @[inline]
                                def Function.curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
                                (α × βφ)αβφ

                                Interpret a function on α × β as a function with two arguments.

                                Equations
                                Instances For
                                  @[inline]
                                  def Function.uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} :
                                  (αβφ)α × βφ

                                  Interpret a function with two arguments as a function on α × β

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Function.curry_uncurry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : αβφ) :
                                    @[simp]
                                    theorem Function.uncurry_curry {α : Type u₁} {β : Type u₂} {φ : Type u₃} (f : α × βφ) :
                                    theorem Function.LeftInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : Function.LeftInverse g f) :
                                    g f = id
                                    theorem Function.RightInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : Function.RightInverse g f) :
                                    f g = id
                                    def Function.IsFixedPt {α : Type u₁} (f : αα) (x : α) :

                                    A point x is a fixed point of f : α → α if f x = x.

                                    Equations
                                    Instances For