Nuprl Lemma : isect2_quotient

[T:Type]. ∀[E1,E2:T ⟶ T ⟶ ℙ].
  (x,y:T//E1[x;y] ⋂ x,y:T//E2[x;y] ≡ x,y:T//(E1[x;y] ∧ E2[x;y])) supposing 
     (EquivRel(T;x,y.E1[x;y]) and 


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] and: P ∧ Q function: x:A ⟶ B[x] 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 so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] prop: implies:  Q all: x:A. B[x] cand: c∧ B guard: {T} bfalse: ff ifthenelse: if then else fi  btrue: tt it: unit: Unit bool: 𝔹 isect2: T1 ⋂ T2 quotient: x,y:A//B[x; y]
Lemmas referenced :  equiv_rel_wf istype-universe subtype_by_equality isect2_wf quotient_wf equiv_rel_and istype-base isect2_decomp isect2_subtype_rel2 equal_functionality_wrt_subtype_rel2 isect2_subtype_rel base_wf quotient-isect-base2 quotient-member-eq subtype_rel_self bool_wf equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut independent_pairFormation sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality axiomEquality hypothesis Error :universeIsType,  extract_by_obid isectElimination hypothesisEquality Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :functionIsType,  because_Cache universeEquality instantiate independent_isectElimination productEquality independent_functionElimination Error :lambdaFormation_alt,  Error :equalityIstype,  sqequalBase equalitySymmetry equalityTransitivity functionExtensionality cumulativity equalityElimination unionElimination isect_memberEquality pertypeElimination promote_hyp dependent_functionElimination Error :productIsType,  lambdaEquality pointwiseFunctionalityForEquality lemma_by_obid

\mforall{}[T:Type].  \mforall{}[E1,E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (x,y:T//E1[x;y]  \mcap{}  x,y:T//E2[x;y]  \mequiv{}  x,y:T//(E1[x;y]  \mwedge{}  E2[x;y]))  supposing 
          (EquivRel(T;x,y.E1[x;y])  and 

Date html generated: 2019_06_20-PM-00_32_28
Last ObjectModification: 2018_11_25-PM-01_55_03

Theory : quot_1

Home Index