Nuprl Lemma : extd-nameset_subtype_base

[L:Cname List]. (extd-nameset(L) ⊆Base)


Proof




Definitions occuring in Statement :  extd-nameset: extd-nameset(L) coordinate_name: Cname list: List subtype_rel: A ⊆B uall: [x:A]. B[x] base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T extd-nameset: extd-nameset(L) b-union: A ⋃ B so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a all: x:A. B[x] ifthenelse: if then else fi  bool: 𝔹 int_seg: {i..j-} subtype_rel: A ⊆B
Lemmas referenced :  tunion_subtype_base bool_wf ifthenelse_wf nameset_wf int_seg_wf nameset_subtype_base set_subtype_base lelt_wf int_subtype_base list_wf coordinate_name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality instantiate hypothesisEquality universeEquality natural_numberEquality independent_isectElimination lambdaFormation unionElimination intEquality because_Cache axiomEquality

Latex:
\mforall{}[L:Cname  List].  (extd-nameset(L)  \msubseteq{}r  Base)



Date html generated: 2016_05_20-AM-09_28_59
Last ObjectModification: 2015_12_28-PM-04_47_57

Theory : cubical!sets


Home Index