Nuprl Lemma : member-per-union-right

[A,B:Type]. ∀[x:B].  (inr x  ∈ per-union(A;B))


Proof




Definitions occuring in Statement :  per-union: per-union(A;B) uall: [x:A]. B[x] member: t ∈ T inr: inr  universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T per-union: per-union(A;B) has-value: (a)↓ outr: outr(x) uimplies: supposing a prop: true: True uand: uand(A;B) top: Top squash: T subtype_rel: A ⊆B
Lemmas referenced :  per-union_wf has-value_wf_base is-exception_wf uand_wf sqle_wf_base top_wf base_wf equal_wf squash_wf true_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut pointwiseFunctionality sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry hypothesisEquality isect_memberEquality isectElimination thin because_Cache universeEquality extract_by_obid axiomSqleEquality divergentSqle sqleReflexivity baseClosed baseApply closedConclusion pertypeMemberEquality natural_numberEquality rename isaxiomCases axiomSqEquality voidElimination voidEquality applyEquality lambdaEquality imageElimination imageMemberEquality instantiate

Latex:
\mforall{}[A,B:Type].  \mforall{}[x:B].    (inr  x    \mmember{}  per-union(A;B))



Date html generated: 2019_06_20-AM-11_30_54
Last ObjectModification: 2018_08_01-PM-05_11_41

Theory : per!type


Home Index