Nuprl Lemma : isect_prod_lemma
∀[A,B,C:Type]. (A × B ⋂ A × C ⊆r (A × B ⋂ C))
Proof
Definitions occuring in Statement :
isect2: T1 ⋂ T2,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
isect2: T1 ⋂ T2,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
ifthenelse: if b then t else f fi ,
bfalse: ff,
prop: ℙ,
pi2: snd(t),
pi1: fst(t),
implies: P ⇒ Q,
all: ∀x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
member: t ∈ T
Lemmas referenced :
equal_wf,
isect2_decomp,
isect2_wf
Rules used in proof :
independent_pairEquality,
Error :lambdaFormation_alt,
Error :equalityIstype,
Error :isect_memberEquality_alt,
unionElimination,
equalityElimination,
because_Cache,
independent_functionElimination,
dependent_functionElimination,
sqequalRule,
lambdaFormation,
productElimination,
equalityTransitivity,
equalitySymmetry,
independent_pairFormation,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaEquality_alt,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
productEquality,
hypothesisEquality,
hypothesis,
Error :inhabitedIsType,
universeEquality
Latex:
\mforall{}[A,B,C:Type]. (A \mtimes{} B \mcap{} A \mtimes{} C \msubseteq{}r (A \mtimes{} B \mcap{} C))
Date html generated:
2019_06_20-PM-01_04_51
Last ObjectModification:
2019_06_20-PM-01_00_45
Theory : bool_1
Home
Index