### Nuprl Lemma : strong-continuity2-half-squash

`∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)`

Proof

Definitions occuring in Statement :  strong-continuity2: `strong-continuity2(T;F)` quotient: `x,y:A//B[x; y]` nat: `ℕ` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` squash: `↓T` and: `P ∧ Q` true: `True` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` and: `P ∧ Q` subtype_rel: `A ⊆r B` squash: `↓T` all: `∀x:A. B[x]` prop: `ℙ` sq-basic-strong-continuity: `sq-basic-strong-continuity(T;F)` sq_exists: `∃x:A [B[x]]` basic-strong-continuity: `basic-strong-continuity(T;F)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` implies: `P `` Q` guard: `{T}`
Lemmas referenced :  Kleene-M_wf subtype_rel_wf nat_wf squash_wf subtype_rel_self quotient_wf basic-strong-continuity_wf true_wf equiv_rel_true implies-quotient-true2 strong-continuity2_wf trivial-quotient-true basic-implies-strong-continuity2-ext istype-nat istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality hypothesis imageElimination imageMemberEquality hypothesisEquality baseClosed rename Error :lambdaFormation_alt,  extract_by_obid isectElimination Error :dependent_set_memberEquality_alt,  Error :productIsType,  Error :universeIsType,  applyEquality Error :lambdaEquality_alt,  Error :inhabitedIsType,  independent_isectElimination independent_functionElimination because_Cache Error :functionIsType,  instantiate universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(strong-continuity2(T;F))  supposing  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)

Date html generated: 2019_06_20-PM-02_51_16
Last ObjectModification: 2019_02_09-PM-11_56_09

Theory : continuity

Home Index