Nuprl Lemma : induced-rmetric_wf
∀[Y:Type]. ∀[f:Y ⟶ ℝ]. (induced-rmetric(f) ∈ metric(Y))
Proof
Definitions occuring in Statement :
induced-rmetric: induced-rmetric(f),
metric: metric(X),
real: ℝ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
induced-rmetric: induced-rmetric(f),
induced-metric: induced-metric(d;f),
rabs: |x|,
rmetric: rmetric()
Lemmas referenced :
induced-metric_wf,
real_wf,
rmetric_wf,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesis,
isect_memberFormation_alt,
hypothesisEquality,
functionIsType,
universeIsType,
instantiate,
universeEquality,
sqequalRule,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[Y:Type]. \mforall{}[f:Y {}\mrightarrow{} \mBbbR{}]. (induced-rmetric(f) \mmember{} metric(Y))
Date html generated:
2019_10_29-AM-11_04_55
Last ObjectModification:
2019_10_02-AM-09_46_37
Theory : reals
Home
Index