Graph

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

theorem Function.Graph₂.eq {σ : Sort u_1} {α : Sort u_2} {β : Sort u_3} {f : α → β → σ} {y : σ} {x₁ : α} {x₂ : β} (h : 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 ↔ 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₂ ↔ 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 : 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 ↔ 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₃ ↔ Graph₃ f y x₁ x₂ x₃