### Nuprl Lemma : unit-interval-fan_wf

`∀[f:ℕ ⟶ 𝔹]. ∀[n:ℕ].  (unit-interval-fan(f;n) ∈ ℤ × ℤ)`

Proof

Definitions occuring in Statement :  unit-interval-fan: `unit-interval-fan(f;n)` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` product: `x:A × B[x]` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` unit-interval-fan: `unit-interval-fan(f;n)` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` has-value: `(a)↓` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  primrec_wf nat_wf int_seg_subtype_nat false_wf bool_wf eqtt_to_assert value-type-has-value int-value-type eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin productEquality intEquality because_Cache hypothesisEquality independent_pairEquality natural_numberEquality lambdaEquality productElimination applyEquality functionExtensionality hypothesis setElimination rename independent_isectElimination independent_pairFormation lambdaFormation unionElimination equalityElimination callbyvalueReduce addEquality multiplyEquality equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination axiomEquality isect_memberEquality functionEquality

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].    (unit-interval-fan(f;n)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{})

Date html generated: 2017_10_03-AM-09_48_31
Last ObjectModification: 2017_07_28-AM-08_00_34

Theory : reals

Home Index