Documentation

Arithmetization.Vorspiel.Graph

def Function.Graphᵥ {α : Sort u_2} {k : } (f : (Fin kα)α) :
(Fin (k + 1)α)Prop
Equations
Instances For
    def Function.Graph {σ : Sort u_1} {α : Sort u_2} (f : ασ) :
    σαProp
    Equations
    Instances For
      def Function.Graph₂ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} (f : αβσ) :
      σαβProp
      Equations
      Instances For
        def Function.Graph₃ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (f : αβγσ) :
        σαβγProp
        Equations
        Instances For
          def Function.Graph₄ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {δ : Sort u_5} (f : αβγδσ) :
          σαβγδProp
          Equations
          Instances For
            def Function.Graph₅ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {δ : Sort u_5} {ε : Sort u_6} (f : αβγδεσ) :
            σαβγδεProp
            Equations
            Instances For
              theorem Function.Graph.eq {σ : Sort u_1} {α : Sort u_2} {f : ασ} {y : σ} {x : α} (h : Function.Graph f y x) :
              f x = y
              theorem Function.Graph.iff_left {σ : Sort u_1} {α : Sort u_2} (f : ασ) {y : σ} {x : α} :
              f x = y Function.Graph f y x
              theorem Function.Graph.iff_right {σ : Sort u_1} {α : Sort u_2} (f : ασ) {y : σ} {x : α} :
              y = f x Function.Graph f y x
              theorem Function.Graph₂.eq {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {f : αβσ} {y : σ} {x₁ : α} {x₂ : β} (h : Function.Graph₂ f y x₁ x₂) :
              f x₁ x₂ = y
              theorem Function.Graph₂.iff_left {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} (f : αβσ) {y : σ} {x₁ : α} {x₂ : β} :
              f x₁ x₂ = y Function.Graph₂ f y x₁ x₂
              theorem Function.Graph₂.iff_right {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} (f : αβσ) {y : σ} {x₁ : α} {x₂ : β} :
              y = f x₁ x₂ Function.Graph₂ f y x₁ x₂
              theorem Function.Graph₃.eq {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {f : αβγσ} {y : σ} {x₁ : α} {x₂ : β} {x₃ : γ} (h : Function.Graph₃ f y x₁ x₂ x₃) :
              f x₁ x₂ x₃ = y
              theorem Function.Graph₃.iff_left {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (f : αβγσ) {y : σ} {x₁ : α} {x₂ : β} {x₃ : γ} :
              f x₁ x₂ x₃ = y Function.Graph₃ f y x₁ x₂ x₃
              theorem Function.Graph₃.iff_right {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (f : αβγσ) {y : σ} {x₁ : α} {x₂ : β} {x₃ : γ} :
              y = f x₁ x₂ x₃ Function.Graph₃ f y x₁ x₂ x₃