### Nuprl Lemma : all-quotient-true3

`∀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 :  all: `∀x:A. B[x]` implies: `P `` Q` canonicalizable: `canonicalizable(T)` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` rev_implies: `P `` Q` guard: `{T}` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff`
Lemmas referenced :  iff_weakening_equal implies-quotient-true equiv_rel_true true_wf quotient_wf all_wf subtype_rel_self isect2_subtype_rel subtype_rel_dep_function isect2_subtype_rel2 base_wf isect2_wf all-quotient-true2 canonicalizable_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin functionEquality cumulativity hypothesisEquality universeEquality cut lemma_by_obid isectElimination hypothesis dependent_functionElimination independent_functionElimination applyEquality instantiate sqequalRule lambdaEquality independent_isectElimination independent_pairFormation functionExtensionality because_Cache isect_memberEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}T:Type.  (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: 2016_05_14-PM-09_42_10
Last ObjectModification: 2016_05_10-AM-11_31_10

Theory : continuity

Home Index