Nuprl Lemma : set-sig-singleton_wf

[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-singleton(s) ∈ Item ─→ set-sig-set(s))


Proof




Definitions occuring in Statement :  set-sig-singleton: set-sig-singleton(s) set-sig-set: set-sig-set(s) set-sig: set-sig{i:l}(Item) uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  subtype_rel_self valueall-type_wf bool_wf all_wf not_wf assert_wf iff_wf equal_wf or_wf set-sig_wf
\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].    (set-sig-singleton(s)  \mmember{}  Item  {}\mrightarrow{}  set-sig-set(s))



Date html generated: 2015_07_17-AM-08_21_12
Last ObjectModification: 2015_04_02-PM-05_42_55

Home Index