Nuprl Lemma : frequency_wf

`∀[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹]. ∀[f:ℕ ⟶ T]. ∀[x:T]. ∀[p:ℕ]. ∀[q:ℕ+].  (frequency(f;x) ~ (p/q) ∈ ℙ)`

Proof

Definitions occuring in Statement :  frequency: `frequency(f;x) ~ (p/q)` nat_plus: `ℕ+` nat: `ℕ` bool: `𝔹` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  frequency: `frequency(f;x) ~ (p/q)` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` cand: `A c∧ B` nat: `ℕ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` nat_plus: `ℕ+` guard: `{T}` so_apply: `x[s]`
Lemmas referenced :  all_wf nat_wf exists_wf less_than_wf ratio-dist_wf seq-count_wf int_seg_subtype_nat false_wf less_than_transitivity2 nat_plus_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality because_Cache productEquality setElimination rename hypothesisEquality cumulativity applyEquality natural_numberEquality addEquality independent_isectElimination independent_pairFormation lambdaFormation dependent_set_memberEquality productElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[x:T].  \mforall{}[p:\mBbbN{}].  \mforall{}[q:\mBbbN{}\msupplus{}].    (frequency(f;x)  \msim{}  (p/q)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_15-PM-04_44_07
Last ObjectModification: 2015_12_27-PM-02_39_13

Theory : general

Home Index