### Nuprl Lemma : ucont_wf

`∀[T:Type]. ∀[F:(ℕ ⟶ 𝔹) ⟶ T]. ∀[M:⇃(∃M:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ (T?) [(∀f:ℕ ⟶ 𝔹`
`                                                                     ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (T?)))`
`                                                                     ∧ (∀n:ℕ`
`                                                                          (M n f) = (inl (F f)) ∈ (T?) `
`                                                                          supposing ↑isl(M n f))))])].`
`  (ucont(F;M) ∈ ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) `` ((F f) = (F g) ∈ T))))`

Proof

Definitions occuring in Statement :  ucont: `ucont(F;M)` quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` assert: `↑b` isl: `isl(x)` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` true: `True` unit: `Unit` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` inl: `inl x` union: `left + right` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` ucont: `ucont(F;M)` uniform-continuity-from-fan-ext subtype_rel: `A ⊆r B` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` nat: `ℕ` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` exists: `∃x:A. B[x]` isl: `isl(x)` so_apply: `x[s]` sq_exists: `∃x:A [B[x]]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  uniform-continuity-from-fan-ext bool_wf quotient_wf sq_exists_wf nat_wf int_seg_wf unit_wf2 equal_wf assert_wf btrue_wf bfalse_wf istype-nat true_wf istype-assert equiv_rel_true isl_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule applyEquality thin instantiate extract_by_obid hypothesis Error :lambdaEquality_alt,  isectElimination hypothesisEquality equalityTransitivity equalitySymmetry Error :isectIsType,  Error :inhabitedIsType,  Error :functionIsType,  because_Cache Error :universeIsType,  sqequalHypSubstitution functionEquality natural_numberEquality setElimination rename unionEquality productEquality Error :inlEquality_alt,  isectEquality Error :lambdaFormation_alt,  unionElimination Error :equalityIstype,  dependent_functionElimination independent_functionElimination Error :unionIsType,  Error :setIsType,  Error :productIsType,  independent_isectElimination axiomEquality Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T].  \mforall{}[M:\00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  (T?)  [(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}
((\mexists{}n:\mBbbN{}
((M  n  f)  =  (inl  (F  f))))
\mwedge{}  (\mforall{}n:\mBbbN{}
(M  n  f)  =  (inl  (F  f))
supposing  \muparrow{}isl(M  n
f))))])].
(ucont(F;M)  \mmember{}  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))))

Date html generated: 2019_06_20-PM-02_52_39
Last ObjectModification: 2019_01_26-PM-06_13_12

Theory : continuity

Home Index