Nuprl Lemma : quotient-top-union-top
⇃(Top + Top) ⋂ Base ⊆r (Top + Top)
Proof
Definitions occuring in Statement :
isect2: T1 ⋂ T2,
quotient: x,y:A//B[x; y],
subtype_rel: A ⊆r B,
top: Top,
true: True,
union: left + right,
base: Base
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
guard: {T},
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
quotient-isect-base,
top_wf,
true_wf,
equiv_rel_true,
isect2_wf,
quotient_wf,
base_wf,
isect2_subtype_rel,
subtype_rel_functionality_wrt_iff,
ext-eq_weakening
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
unionEquality,
hypothesis,
sqequalRule,
lambdaEquality,
independent_isectElimination,
because_Cache,
productElimination
Latex:
\00D9(Top + Top) \mcap{} Base \msubseteq{}r (Top + Top)
Date html generated:
2018_05_21-PM-00_04_54
Last ObjectModification:
2018_05_19-AM-07_09_57
Theory : quot_1
Home
Index