### Nuprl Lemma : all_quot_elim

`∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].`
`  (EquivRel(T;x,y.E[x;y])`
`  `` (∀[F:(x,y:T//E[x;y]) ⟶ ℙ]. ((∀w:x,y:T//E[x;y]. SqStable(F w)) `` (∀z:x,y:T//E[x;y]. F[z] `⇐⇒` ∀z:T. F[z]))))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  quotient: `x,y:A//B[x; y]` squash: `↓T` guard: `{T}` sq_stable: `SqStable(P)` uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` so_apply: `x[s]` so_apply: `x[s1;s2]`
Lemmas referenced :  squash_wf equal_wf equal-wf-base subtype_rel_self all_wf quotient_wf subtype_quotient sq_stable_wf equiv_rel_wf
Rules used in proof :  pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry because_Cache rename imageMemberEquality baseClosed productEquality instantiate independent_functionElimination dependent_functionElimination isect_memberFormation lambdaFormation independent_pairFormation hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin lambdaEquality applyEquality independent_isectElimination hypothesis functionEquality cumulativity universeEquality sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
(EquivRel(T;x,y.E[x;y])
{}\mRightarrow{}  (\mforall{}[F:(x,y:T//E[x;y])  {}\mrightarrow{}  \mBbbP{}]
((\mforall{}w:x,y:T//E[x;y].  SqStable(F  w))  {}\mRightarrow{}  (\mforall{}z:x,y:T//E[x;y].  F[z]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:T.  F[z]))))

Date html generated: 2019_06_20-PM-01_05_18
Last ObjectModification: 2019_06_20-PM-00_59_36

Theory : quot_1

Home Index