Equations
- Function.Graph f y x = (y = f x)
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
Equations
- Function.Graph₃ f y x₁ x₂ x₃ = (y = f x₁ x₂ x₃)
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₃