Nuprl Definition : real-disjoint
real-disjoint(x.A[x];y.B[y]) == ∀x,y:ℝ. ((x = y) ⇒ (¬(A[x] ∧ B[y])))
Definitions occuring in Statement :
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
real: ℝ,
implies: P ⇒ Q,
req: x = y,
not: ¬A,
and: P ∧ Q
FDL editor aliases :
real-disjoint
Latex:
real-disjoint(x.A[x];y.B[y]) == \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (\mneg{}(A[x] \mwedge{} B[y])))
Date html generated:
2017_10_03-AM-10_00_24
Last ObjectModification:
2017_06_30-AM-10_49_01
Theory : reals
Home
Index