Nuprl Lemma : uniform-continuity-from-fan2

[T:Type]
((∃U:Type. ((U ⊆r ℕ) ∧ (∃r:ℕ ⟶ U. ∀x:U. ((r x) x ∈ U)) ∧ (∃h:T ⟶ U. Bij(T;U;h))))
(∀F:(ℕ ⟶ 𝔹) ⟶ T. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f g ∈ (ℕn ⟶ 𝔹))  ((F f) (F g) ∈ T)))))

Proof

Definitions occuring in Statement :  biject: Bij(A;B;f) quotient: x,y:A//B[x; y] int_seg: {i..j-} nat: bool: 𝔹 subtype_rel: A ⊆B uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q true: True apply: a function: x:A ⟶ B[x] natural_number: \$n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T exists: x:A. B[x] and: P ∧ Q subtype_rel: A ⊆B prop: nat: uimplies: supposing a le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A isl: isl(x) so_lambda: λ2x.t[x] so_apply: x[s] sq_exists: x:A [B[x]] guard: {T}
Lemmas referenced :  uniform-continuity-from-fan strong-continuity2-half-squash-surject-biject bool_wf surject-nat-bool biject_wf implies-quotient-true nat_wf int_seg_wf unit_wf2 equal_wf subtype_rel_function int_seg_subtype_nat istype-false subtype_rel_self assert_wf btrue_wf bfalse_wf sq_exists_wf istype-nat istype-assert subtype_rel_wf istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination independent_functionElimination productElimination hypothesis Error :dependent_pairFormation_alt,  sqequalRule Error :functionIsType,  Error :universeIsType,  Error :equalityIstype,  because_Cache applyEquality productEquality functionEquality natural_numberEquality setElimination rename unionEquality independent_isectElimination independent_pairFormation Error :inlEquality_alt,  isectEquality Error :inhabitedIsType,  unionElimination equalityTransitivity equalitySymmetry Error :lambdaEquality_alt,  Error :unionIsType,  Error :dependent_set_memberEquality_alt,  Error :productIsType,  Error :isectIsType,  instantiate universeEquality

Latex:
\mforall{}[T:Type]
((\mexists{}U:Type.  ((U  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mexists{}r:\mBbbN{}  {}\mrightarrow{}  U.  \mforall{}x:U.  ((r  x)  =  x))  \mwedge{}  (\mexists{}h:T  {}\mrightarrow{}  U.  Bij(T;U;h))))
{}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.  \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_26
Last ObjectModification: 2019_02_06-PM-04_01_15

Theory : continuity

Home Index