Documentation
Marginis
.
PaulyZiegler2013
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Complex.Basic
Mathlib.Data.Fin.Basic
Mathlib.Data.Real.Basic
Mathlib.LinearAlgebra.Matrix.Trace
Imported by
Henkin
l₀
l₁
zero_not_enough
one_not_enough
source
def
Henkin
{n :
ℕ
}
{U :
Type
}
(R :
(
Fin
n
→
U
)
→
(
Fin
n
→
U
)
→
Prop
)
:
Prop
Equations
Henkin
R
=
∃ (
Y
:
Fin
n
→
U
→
U
),
∀ (
x
:
Fin
n
→
U
),
R
x
fun (
k
:
Fin
n
) =>
Y
k
(
x
k
)
Instances For
source
theorem
l₀
{U :
Sort
u_1}
(x :
Fin
0
→
U
)
(y :
Fin
0
→
U
)
:
x
=
y
source
theorem
l₁
{U :
Sort
u_1}
(a :
Fin
0
→
U
)
(x :
Fin
0
→
U
)
(R :
(
Fin
0
→
U
)
→
(
Fin
0
→
U
)
→
Prop
)
(y :
Fin
0
→
U
)
:
R
a
x
→
R
a
y
source
theorem
zero_not_enough
:
¬
∃ (
U
:
Type
) (
R
:
(
Fin
0
→
U
)
→
(
Fin
0
→
U
)
→
Prop
),
(∀ (
x
:
Fin
0
→
U
),
∃ (
y
:
Fin
0
→
U
),
R
x
y
)
∧
¬
Henkin
R
source
theorem
one_not_enough
:
¬
∃ (
U
:
Type
) (
R
:
(
Fin
1
→
U
)
→
(
Fin
1
→
U
)
→
Prop
),
(∀ (
x
:
Fin
1
→
U
),
∃ (
y
:
Fin
1
→
U
),
R
x
y
)
∧
¬
Henkin
R