### 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 `
`     EquivRel(T;x,y.E2[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: `b 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: `b supposing a` ext-eq: `A ≡ B` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` prop: `ℙ` implies: `P `` Q` all: `∀x:A. B[x]` cand: `A c∧ B` guard: `{T}` bfalse: `ff` ifthenelse: `if b then t else f 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

Latex:
\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
EquivRel(T;x,y.E2[x;y]))

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

Theory : quot_1

Home Index