Nuprl Lemma : circle-param_wf

[t:ℝ]. (circle-param(t) ∈ {p:ℝ^2| r2-unit-circle(p)} )


Proof




Definitions occuring in Statement :  circle-param: circle-param(t) r2-unit-circle: r2-unit-circle(p) real-vec: ^n real: uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q uiff: uiff(P;Q) uimplies: supposing a prop: all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True rge: x ≥ y guard: {T} circle-param: circle-param(t) real-vec: ^n int_seg: {i..j-} bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  rneq: x ≠ y or: P ∨ Q bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb assert: b false: False r2-unit-circle: r2-unit-circle(p) eq_int: (i =z j) nat: le: A ≤ B not: ¬A rev_uimplies: rev_uimplies(P;Q) rdiv: (x/y) req_int_terms: t1 ≡ t2 top: Top
Lemmas referenced :  square-nonneg trivial-rleq-radd int-to-real_wf rmul_wf r2-unit-circle_wf real_wf radd_wf rless-int rless_functionality_wrt_implies rleq_weakening_equal eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int rdiv_wf rsub_wf rless_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int int_seg_wf rnexp_wf false_wf le_wf req_functionality radd_functionality rnexp2 req_weakening rmul_preserves_req rinv_wf2 itermSubtract_wf itermMultiply_wf itermAdd_wf itermConstant_wf itermVar_wf req-iff-rsub-is-0 rmul-identity1 req_transitivity rmul-rinv3 rmul_functionality rinv-mul-as-rdiv rinv-as-rdiv real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_add_lemma real_term_value_const_lemma real_term_value_var_lemma rmul-rinv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis natural_numberEquality productElimination independent_isectElimination dependent_set_memberEquality sqequalRule axiomEquality equalityTransitivity equalitySymmetry because_Cache dependent_functionElimination independent_functionElimination independent_pairFormation imageMemberEquality baseClosed lambdaEquality setElimination rename lambdaFormation unionElimination equalityElimination inrFormation dependent_pairFormation promote_hyp instantiate cumulativity voidElimination approximateComputation int_eqEquality intEquality isect_memberEquality voidEquality

Latex:
\mforall{}[t:\mBbbR{}].  (circle-param(t)  \mmember{}  \{p:\mBbbR{}\^{}2|  r2-unit-circle(p)\}  )



Date html generated: 2017_10_03-AM-10_51_29
Last ObjectModification: 2017_06_18-PM-01_24_17

Theory : reals


Home Index