Arithmetization.Vorspiel.Graph

source

def Function.Graphᵥ {α : Sort u_2} {k : ℕ} (f : (Fin k → α) → α) :

(Fin (k + 1) → α) → Prop

Equations

Function.Graphᵥ f v = (v 0 = f fun (x : Fin k) => v x.succ)

Instances For

source

def Function.Graph {σ : Sort u_1} {α : Sort u_2} (f : α → σ) :

σ → α → Prop

Equations

Function.Graph f y x = (y = f x)

Instances For

source

def Function.Graph₂ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} (f : α → β → σ) :

σ → α → β → Prop

Equations

Function.Graph₂ f y x₁ x₂ = (y = f x₁ x₂)

Instances For

source

def Function.Graph₃ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} (f : α → β → γ → σ) :

σ → α → β → γ → Prop

Equations

Function.Graph₃ f y x₁ x₂ x₃ = (y = f x₁ x₂ x₃)

Instances For

source

def Function.Graph₄ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {δ : Sort u_5} (f : α → β → γ → δ → σ) :

σ → α → β → γ → δ → Prop

Equations

Function.Graph₄ f y x₁ x₂ x₃ x₄ = (y = f x₁ x₂ x₃ x₄)

Instances For

source

def Function.Graph₅ {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {γ : Sort u_4} {δ : Sort u_5} {ε : Sort u_6} (f : α → β → γ → δ → ε → σ) :

σ → α → β → γ → δ → ε → Prop

Equations

Function.Graph₅ f y x₁ x₂ x₃ x₄ x₅ = (y = f x₁ x₂ x₃ x₄ x₅)

Instances For

source

theorem Function.Graph.eq {σ : Sort u_1} {α : Sort u_2} {f : α → σ} {y : σ} {x : α} (h : Function.Graph f y x) :

f x = y

source

theorem Function.Graph.iff_left {σ : Sort u_1} {α : Sort u_2} (f : α → σ) {y : σ} {x : α} :

f x = y ↔ Function.Graph f y x

source

theorem Function.Graph.iff_right {σ : Sort u_1} {α : Sort u_2} (f : α → σ) {y : σ} {x : α} :

y = f x ↔ Function.Graph f y x

source

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

source

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₂

source

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₂

source

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

source

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₃

source

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₃