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: b supposing a
, 
less_than: a < b
, 
absval: |i|
, 
equal: s = t ∈ T
, 
apply: f 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:
2019_06_20-PM-04_12_03
Last ObjectModification:
2016_07_08-PM-03_49_09
Theory : rules
Home
Index