Nuprl Definition : Leibniz-type
Leibniz-type{i:l}(T) ==
∃sep:T ⟶ T ⟶ ℙ. ((∀x,y:T. ((sep x y) ⇒ (∀z:T. ((sep x z) ∨ (sep y z))))) ∧ (∀x,y:T. (x = y ∈ T ⇐⇒ ¬(sep x y))))
Definitions occuring in Statement :
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
and: P ∧ Q,
implies: P ⇒ Q,
or: P ∨ Q,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
equal: s = t ∈ T,
not: ¬A,
apply: f a
FDL editor aliases :
Leibniz-type
Latex:
Leibniz-type\{i:l\}(T) ==
\mexists{}sep:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
((\mforall{}x,y:T. ((sep x y) {}\mRightarrow{} (\mforall{}z:T. ((sep x z) \mvee{} (sep y z))))) \mwedge{} (\mforall{}x,y:T. (x = y \mLeftarrow{}{}\mRightarrow{} \mneg{}(sep x y))))
Date html generated:
2019_10_31-AM-07_25_46
Last ObjectModification:
2019_09_19-PM-04_35_32
Theory : constructive!algebra
Home
Index