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

      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, 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
            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, inline]
                  abbrev Function.swap {α : Sort u₁} {β : Sort u₂} {φ : αβSort u₃} (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
                  φ x y

                  For a two-argument function f, swap f is the same function but taking the arguments in the reverse order. swap f y x = f x y.

                  Equations
                    Instances For
                      theorem Function.swap_def {α : Sort u₁} {β : Sort u₂} {φ : αβSort u₃} (f : (x : α) → (y : β) → φ x y) :
                      swap f = fun (y : β) (x : α) => f x y
                      theorem Function.comp_assoc {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φδ) (g : βφ) (h : αβ) :
                      (f g) h = f g h
                      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 : Injective g) (hf : 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 : Surjective g) (hf : 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 : αβ} :
                                  Bijective gBijective fBijective (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 : Injective f) (lfg : LeftInverse f g) :
                                                  theorem Function.RightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (h : RightInverse g f) :
                                                  theorem Function.HasRightInverse.surjective {α : Sort u₁} {β : Sort u₂} {f : αβ} :
                                                  theorem Function.leftInverse_of_surjective_of_rightInverse {α : Sort u₁} {β : Sort u₂} {f : αβ} {g : βα} (surjf : Surjective f) (rfg : RightInverse f g) :
                                                  theorem Function.Injective.eq_iff {α : Sort u₁} {β : Sort u₂} {f : αβ} (I : Injective f) {a b : α} :
                                                  f a = f b a = b
                                                  theorem Function.Injective.beq_eq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : αβ} (I : Injective f) {a b : α} :
                                                  (f a == f b) = (a == b)
                                                  theorem Function.Injective.eq_iff' {α : Sort u₁} {β : Sort u₂} {f : αβ} (I : Injective f) {a b : α} {c : β} (h : f b = c) :
                                                  f a = c a = b
                                                  theorem Function.Injective.ne {α : Sort u₁} {β : Sort u₂} {f : αβ} (hf : Injective f) {a₁ a₂ : α} :
                                                  a₁ a₂f a₁ f a₂
                                                  theorem Function.Injective.ne_iff {α : Sort u₁} {β : Sort u₂} {f : αβ} (hf : Injective f) {x y : α} :
                                                  f x f y x y
                                                  theorem Function.Injective.ne_iff' {α : Sort u₁} {β : Sort u₂} {f : αβ} (hf : Injective f) {x y : α} {z : β} (h : f y = z) :
                                                  f x z x y
                                                  theorem Function.LeftInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : LeftInverse g f) :
                                                  g f = id
                                                  theorem Function.RightInverse.id {α : Type u₁} {β : Type u₂} {g : βα} {f : αβ} (h : 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
                                                      def Pi.map {ι : Sort u_1} {α : ιSort u_2} {β : ιSort u_3} (f : (i : ι) → α iβ i) :
                                                      ((i : ι) → α i)(i : ι) → β i

                                                      Sends a dependent function a : ∀ i, α i to a dependent function Pi.map f a : ∀ i, β i by applying f i to i-th component.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Pi.map_apply {ι : Sort u_1} {α : ιSort u_2} {β : ιSort u_3} (f : (i : ι) → α iβ i) (a : (i : ι) → α i) (i : ι) :
                                                          Pi.map f a i = f i (a i)