Nuprl Rule : Continuity

This rule proved as lemma rule_continuity_true3 in file continuity/continuity_rule_gen.v
 at https://github.com/vrahli/NuprlInCoq  

H  ⊢ ↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) (g i) ∈ ℤ supposing |i| < n

  BY Continuity ()
  
  H  ⊢ F ∈ (ℤ ⟶ ℤ) ⟶ ℤ
  H  ⊢ f ∈ ℤ ⟶ ℤ



Definitions occuring in rule :  squash: T exists: x:A. B[x] nat: uall: [x:A]. B[x] uimplies: supposing a less_than: a < b absval: |i| equal: t ∈ T apply: a member: t ∈ T function: x:A ⟶ B[x] int: axiom: Ax

Latex:
H    \mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  \mforall{}[g:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}].  (F  f)  =  (F  g)  supposing  \mforall{}[i:\mBbbZ{}].  (f  i)  =  (g  i)  supposing  |i|  <  n

    BY  Continuity  ()
   
    H    \mvdash{}  F  \mmember{}  (\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbZ{}
    H    \mvdash{}  f  \mmember{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}



Date html generated: 2016_12_14-AM-08_53_42
Last ObjectModification: 2016_07_08-PM-03_49_09

Theory : rules


Home Index