### Nuprl Lemma : real-subset-metric_wf

`∀[P:ℝ ⟶ ℙ]. (real-subset-metric() ∈ metric(x:ℝ × P[x]))`

Proof

Definitions occuring in Statement :  real-subset-metric: `real-subset-metric()` metric: `metric(X)` real: `ℝ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` product: `x:A × B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` real-subset-metric: `real-subset-metric()` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` top: `Top`
Lemmas referenced :  induced-rmetric_wf real_wf subtype_rel_self pi1_wf_top istype-void
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin productEquality hypothesis applyEquality hypothesisEquality instantiate universeEquality lambdaEquality_alt productElimination independent_pairEquality isect_memberEquality_alt voidElimination productIsType universeIsType because_Cache axiomEquality equalityTransitivity equalitySymmetry functionIsType

Latex:
\mforall{}[P:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].  (real-subset-metric()  \mmember{}  metric(x:\mBbbR{}  \mtimes{}  P[x]))

Date html generated: 2019_10_29-AM-11_05_33
Last ObjectModification: 2019_10_02-AM-09_47_11

Theory : reals

Home Index