Nuprl Definition : reqmatrix
X ≡ Y == ∀i:ℕa. ∀j:ℕb. ((X i j) = (Y i j))
Definitions occuring in Statement :
req: x = y,
int_seg: {i..j-},
all: ∀x:A. B[x],
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
req: x = y,
apply: f a
FDL editor aliases :
reqmatrix
Latex:
X \mequiv{} Y == \mforall{}i:\mBbbN{}a. \mforall{}j:\mBbbN{}b. ((X i j) = (Y i j))
Date html generated:
2019_10_30-AM-08_12_21
Last ObjectModification:
2019_09_19-AM-10_41_54
Theory : reals
Home
Index