Nuprl Rule : StrongContinuity2
This rule proved as lemma rule_strong_continuity_true2_v3_2 in file continuity/stronger_continuity_rule4_v3.v
at https://github.com/vrahli/NuprlInCoq
H
⊢ λn,f. ν(v.F (λx.if (x) < (0) then ⊥ else if (x) < (n) then f x else (exception(v; x)))?v:x.<x, x>) ∈ ⇃({M:n:ℕ ─\000C→ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))|
∀f:ℕ ⟶ T
((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
∧ (∀n,m:ℕ. ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)))} )
BY StrongContinuity2 ()
H ⊢ F ∈ (ℕ ⟶ T) ⟶ ℕ
H ⊢ ↓T
H ⊢ T ⊆r ℕ
Definitions occuring in rule :
quotient: x,y:A//B[x; y],
set: {x:A| B[x]} ,
int_seg: {i..j-},
b-union: A ⋃ B,
product: x:A × B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
uimplies: b supposing a,
equal: s = t ∈ T,
all: ∀x:A. B[x],
le: A ≤ B,
implies: P ⇒ Q,
isint: isint def,
false: False,
true: True,
lambda: λx.A[x],
natural_number: $n,
bottom: ⊥,
less: if (a) < (b) then c else d,
apply: f a,
pair: <a, b>,
member: t ∈ T,
function: x:A ⟶ B[x],
squash: ↓T,
subtype_rel: A ⊆r B,
nat: ℕ,
axiom: Ax
Latex:
H
\mvdash{} \mlambda{}n,f. \mnu{}(v.F ...?v:x.<x, x>) \mmember{} \00D9(\{M:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} (\mBbbN{} \mcup{} (\mBbbN{} \mtimes{} \mBbbN{}))|
\mforall{}f:\mBbbN{} {}\mrightarrow{} T
((\mexists{}n:\mBbbN{}. ((M n f) = (F f)))
\mwedge{} (\mforall{}n:\mBbbN{}. (M n f) = (F f) supposing M n f is an integer)
\mwedge{} (\mforall{}n,m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} M n f is an integer {}\mRightarrow{} M m f is an integer)))\} )
BY StrongContinuity2 ()
H \mvdash{} F \mmember{} (\mBbbN{} {}\mrightarrow{} T) {}\mrightarrow{} \mBbbN{}
H \mvdash{} \mdownarrow{}T
H \mvdash{} T \msubseteq{}r \mBbbN{}
Date html generated:
2019_06_20-PM-04_12_08
Last ObjectModification:
2019_02_11-AM-11_15_39
Theory : rules
Home
Index