Nuprl Lemma : strong-continuous-isect2
∀[F,G:Type ⟶ Type]. (Continuous+(T.F[T] ⋂ G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))
Proof
Definitions occuring in Statement :
strong-type-continuous: Continuous+(T.F[T]),
isect2: T1 ⋂ T2,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
so_lambda: λ2x.t[x],
prop: ℙ,
cand: A c∧ B,
bfalse: ff,
ifthenelse: if b then t else f fi ,
btrue: tt,
it: ⋅,
unit: Unit,
bool: 𝔹,
isect2: T1 ⋂ T2,
subtype_rel: A ⊆r B,
and: P ∧ Q,
ext-eq: A ≡ B,
strong-type-continuous: Continuous+(T.F[T]),
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_apply: x[s],
exists: ∃x:A. B[x]
Lemmas referenced :
isect_subtype_rel_trivial,
nat_wf,
isect2_wf,
isect2_subtype_rel,
subtype_rel_wf,
isect2_subtype_rel2,
bool_wf,
isect2_decomp,
strong-type-continuous_wf
Rules used in proof :
because_Cache,
universeEquality,
cumulativity,
functionEquality,
axiomEquality,
independent_pairEquality,
equalitySymmetry,
equalityTransitivity,
productElimination,
hypothesisEquality,
applyEquality,
isectElimination,
isectEquality,
hypothesis,
lemma_by_obid,
equalityElimination,
thin,
unionElimination,
sqequalHypSubstitution,
isect_memberEquality,
lambdaEquality,
independent_pairFormation,
cut,
introduction,
isect_memberFormation,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution,
extract_by_obid,
independent_isectElimination,
dependent_pairFormation
Latex:
\mforall{}[F,G:Type {}\mrightarrow{} Type].
(Continuous+(T.F[T] \mcap{} G[T])) supposing (Continuous+(T.G[T]) and Continuous+(T.F[T]))
Date html generated:
2019_06_20-PM-00_27_39
Last ObjectModification:
2018_08_07-PM-05_10_05
Theory : subtype_1
Home
Index