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

`∀[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 :  member: `t ∈ T` bfalse: `ff` it: `⋅` strong-continuity2-half-squash implies-quotient-true2 trivial-quotient-true basic-implies-strong-continuity2-ext implies-quotient-true
Lemmas referenced :  strong-continuity2-half-squash implies-quotient-true2 trivial-quotient-true basic-implies-strong-continuity2-ext implies-quotient-true
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

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_18
Last ObjectModification: 2019_03_26-AM-06_46_06

Theory : continuity

Home Index