Nuprl Lemma : disjoint-union-classrel
∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
∀v:A + B. uiff(v ∈ X + Y(e);case v of inl(x) => x ∈ X(e) | inr(x) => x ∈ Y(e) ∧ (∀w:A. (¬w ∈ X(e))))
Proof
Definitions occuring in Statement :
disjoint-union-class: X + Y,
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right,
universe: Type
Lemmas :
sq_stable__uiff,
bag-member_wf,
bag-null_wf,
bool_wf,
eqtt_to_assert,
assert-bag-null,
bag-map_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
equal-wf-T-base,
bag_wf,
all_wf,
not_wf,
sq_stable__bag-member,
sq_stable__and,
sq_stable__all,
sq_stable__not,
squash_wf,
uiff_transitivity,
assert_wf,
btrue_wf,
bfalse_wf,
and_wf,
isl_wf,
btrue_neq_bfalse,
exists_wf,
iff_weakening_uiff,
bag-member-map,
false_wf,
bag-member-empty-iff,
uiff_wf,
iff_transitivity,
bnot_wf,
assert_of_bnot,
empty-bag-iff-no-member,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
eclass_wf
Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E].
\mforall{}v:A + B
uiff(v \mmember{} X + Y(e);case v of inl(x) => x \mmember{} X(e) | inr(x) => x \mmember{} Y(e) \mwedge{} (\mforall{}w:A. (\mneg{}w \mmember{} X(e))))
Date html generated:
2015_07_22-PM-00_14_23
Last ObjectModification:
2015_01_28-AM-10_46_44
Home
Index