Nuprl Definition : approx-per
approx-per(T;x;y) ==
((∃t:Base. ((x ≤ t) ∧ (t ∈ T))) ∧ (∃t:Base. ((y ≤ t) ∧ (t ∈ T))))
∧ (∀t:Base. (((x ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((y ≤ t') ∧ (t' = t ∈ T)))))
∧ (∀t:Base. (((y ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((x ≤ t') ∧ (t' = t ∈ T)))))
Definitions occuring in Statement :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
base: Base,
sqle: s ≤ t,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
exists: ∃x:A. B[x],
base: Base,
and: P ∧ Q,
sqle: s ≤ t,
equal: s = t ∈ T
FDL editor aliases :
approx-per
Latex:
approx-per(T;x;y) ==
((\mexists{}t:Base. ((x \mleq{} t) \mwedge{} (t \mmember{} T))) \mwedge{} (\mexists{}t:Base. ((y \mleq{} t) \mwedge{} (t \mmember{} T))))
\mwedge{} (\mforall{}t:Base. (((x \mleq{} t) \mwedge{} (t \mmember{} T)) {}\mRightarrow{} (\mexists{}t':Base. ((y \mleq{} t') \mwedge{} (t' = t)))))
\mwedge{} (\mforall{}t:Base. (((y \mleq{} t) \mwedge{} (t \mmember{} T)) {}\mRightarrow{} (\mexists{}t':Base. ((x \mleq{} t') \mwedge{} (t' = t)))))
Date html generated:
2018_05_21-PM-00_04_18
Last ObjectModification:
2017_12_30-PM-01_58_33
Theory : rel_1
Home
Index