### Nuprl Lemma : all-quotient-true

`∀T:Type. (⇃(canonicalizable(T)) `` (∀P:T ⟶ ℙ. (∀t:T. ⇃(P[t]) `⇐⇒` ⇃(∀t:T. P[t]))))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` canonicalizable: `canonicalizable(T)` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` true: `True` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  guard: `{T}` true: `True` quotient: `x,y:A//B[x; y]` so_apply: `x[s1;s2;s3]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` rev_implies: `P `` Q`
Lemmas referenced :  prop-truncation-quot implies-quotient-true squash_wf dep-fun-equiv_wf equal-wf-base quotient-member-eq all-quotient-dependent all_wf quotient_wf true_wf equiv_rel_true canonicalizable_wf
Rules used in proof :  productEquality natural_numberEquality pertypeElimination pointwiseFunctionalityForEquality rename productElimination independent_functionElimination dependent_functionElimination promote_hyp sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache hypothesis independent_isectElimination functionEquality universeEquality

Latex:
\mforall{}T:Type.  (\00D9(canonicalizable(T))  {}\mRightarrow{}  (\mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.  (\mforall{}t:T.  \00D9(P[t])  \mLeftarrow{}{}\mRightarrow{}  \00D9(\mforall{}t:T.  P[t]))))

Date html generated: 2017_09_29-PM-06_07_48
Last ObjectModification: 2017_09_07-PM-05_50_23

Theory : continuity

Home Index