Nuprl Lemma : isect-subtype-2
∀[G:Type ⟶ Type]. ∀[A,B:Type]. ∀[F:G[A] ⟶ G[B] ⟶ Type]. ∀[X:G[A]]. ∀[Y:G[B]].
((⋂X:G[A]. ⋂Y:G[B]. F[X;Y]) ⊆r F[X;Y])
Proof
Definitions occuring in Statement :
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
so_apply: x[s],
isect: ⋂x:A. B[x],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_apply: x[s],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ
Lemmas referenced :
equal_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
lambdaEquality,
isectElimination,
sqequalHypSubstitution,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
hypothesis,
thin,
isectEquality,
applyEquality,
functionExtensionality,
universeEquality,
cumulativity,
lambdaFormation,
extract_by_obid,
dependent_functionElimination,
independent_functionElimination,
axiomEquality,
isect_memberEquality,
because_Cache,
functionEquality
Latex:
\mforall{}[G:Type {}\mrightarrow{} Type]. \mforall{}[A,B:Type]. \mforall{}[F:G[A] {}\mrightarrow{} G[B] {}\mrightarrow{} Type]. \mforall{}[X:G[A]]. \mforall{}[Y:G[B]].
((\mcap{}X:G[A]. \mcap{}Y:G[B]. F[X;Y]) \msubseteq{}r F[X;Y])
Date html generated:
2017_10_01-AM-09_10_45
Last ObjectModification:
2017_07_26-PM-04_47_04
Theory : general
Home
Index