Nuprl Definition : equiv-props
equiv-props(L) == ∀i,j:ℕ||L||. (L[i] ⇐⇒ L[j])
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
iff: P ⇐⇒ Q,
select: L[n]
FDL editor aliases :
equiv-props
Latex:
equiv-props(L) == \mforall{}i,j:\mBbbN{}||L||. (L[i] \mLeftarrow{}{}\mRightarrow{} L[j])
Date html generated:
2019_06_20-PM-01_49_59
Last ObjectModification:
2019_03_26-AM-10_19_28
Theory : list_1
Home
Index