Nuprl Lemma : quotient-isect-base

[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  x,y:T//E[x;y] ⋂ Base ≡ T ⋂ Base supposing EquivRel(T;x,y.E[x;y])


Proof




Definitions occuring in Statement :  equiv_rel: EquivRel(T;x,y.E[x; y]) isect2: T1 ⋂ T2 quotient: x,y:A//B[x; y] ext-eq: A ≡ B uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] function: x:A ⟶ B[x] base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B isect2: T1 ⋂ T2 bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] cand: c∧ B bfalse: ff or: P ∨ Q prop: quotient: x,y:A//B[x; y]
Lemmas referenced :  isect2_decomp quotient_wf istype-universe base_wf isect2_subtype_rel2 bool_wf isect2_wf isect2_subtype_rel3 subtype_quotient subtype_rel_wf equiv_rel_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation Error :lambdaEquality_alt,  isect_memberEquality sqequalHypSubstitution unionElimination thin equalityElimination sqequalRule extract_by_obid isectElimination because_Cache applyEquality hypothesisEquality Error :inhabitedIsType,  hypothesis independent_isectElimination productElimination equalityTransitivity equalitySymmetry Error :universeIsType,  Error :inlFormation_alt,  independent_pairEquality axiomEquality Error :isect_memberEquality_alt,  Error :functionIsType,  universeEquality pertypeElimination Error :productIsType,  Error :equalityIsType4,  instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    x,y:T//E[x;y]  \mcap{}  Base  \mequiv{}  T  \mcap{}  Base  supposing  EquivRel(T;x,y.E[x;y])



Date html generated: 2019_06_20-PM-00_32_20
Last ObjectModification: 2018_10_06-PM-03_56_25

Theory : quot_1


Home Index