Nuprl Lemma : interval-metric-space_wf
∀[I:Interval]. (interval-metric-space(I) ∈ MetricSpace)
Proof
Definitions occuring in Statement :
interval-metric-space: interval-metric-space(I),
metric-space: MetricSpace,
interval: Interval,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
interval-metric-space: interval-metric-space(I),
metric-space: MetricSpace,
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a
Lemmas referenced :
real_wf,
i-member_wf,
rmetric_wf,
metric-on-subtype,
metric_wf,
interval_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
dependent_pairEquality_alt,
setEquality,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
independent_isectElimination,
lambdaEquality_alt,
setElimination,
rename,
setIsType,
universeIsType,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[I:Interval]. (interval-metric-space(I) \mmember{} MetricSpace)
Date html generated:
2019_10_29-AM-11_12_55
Last ObjectModification:
2019_10_02-AM-09_53_19
Theory : reals
Home
Index