Nuprl Definition : metric-subspace
metric-subspace(X;d;A) == strong-subtype(A;X) ∧ (∀a:A. ∀x:X. (x ≡ a ⇒ (x ∈ A)))
Definitions occuring in Statement :
meq: x ≡ y,
strong-subtype: strong-subtype(A;B),
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
strong-subtype: strong-subtype(A;B),
all: ∀x:A. B[x],
implies: P ⇒ Q,
meq: x ≡ y,
member: t ∈ T
FDL editor aliases :
metric-subspace
Latex:
metric-subspace(X;d;A) == strong-subtype(A;X) \mwedge{} (\mforall{}a:A. \mforall{}x:X. (x \mequiv{} a {}\mRightarrow{} (x \mmember{} A)))
Date html generated:
2019_10_30-AM-06_30_06
Last ObjectModification:
2019_10_02-AM-10_05_06
Theory : reals
Home
Index