Nuprl Definition : real-separation
real-separation(x.A[x];y.B[y]) == real-disjoint(x.A[x];y.B[y]) ∧ (∃x:ℝ. A[x]) ∧ (∃y:ℝ. B[y]) ∧ (∀r:ℝ. (A[r] ∨ B[r]))
Definitions occuring in Statement :
real-disjoint: real-disjoint(x.A[x];y.B[y]),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q
Definitions occuring in definition :
real-disjoint: real-disjoint(x.A[x];y.B[y]),
and: P ∧ Q,
exists: ∃x:A. B[x],
all: ∀x:A. B[x],
real: ℝ,
or: P ∨ Q
FDL editor aliases :
real-separation
Latex:
real-separation(x.A[x];y.B[y]) ==
real-disjoint(x.A[x];y.B[y]) \mwedge{} (\mexists{}x:\mBbbR{}. A[x]) \mwedge{} (\mexists{}y:\mBbbR{}. B[y]) \mwedge{} (\mforall{}r:\mBbbR{}. (A[r] \mvee{} B[r]))
Date html generated:
2017_10_03-AM-10_00_51
Last ObjectModification:
2017_06_30-AM-10_52_51
Theory : reals
Home
Index