Nuprl Lemma : rec-combined-class-0_wf

[Info,A:Type]. ∀[F:bag(A) ─→ bag(A)].  (rec-combined-class-0(F) ∈ EClass(A))


Proof




Definitions occuring in Statement :  rec-combined-class-0: rec-combined-class-0(b) eclass: EClass(A[eo; e]) uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type bag: bag(T)
Lemmas :  stuck-spread base_wf rec-combined-class_wf false_wf le_wf less_than_transitivity1 less_than_irreflexivity int_seg_wf bag_wf

Latex:
\mforall{}[Info,A:Type].  \mforall{}[F:bag(A)  {}\mrightarrow{}  bag(A)].    (rec-combined-class-0(F)  \mmember{}  EClass(A))



Date html generated: 2015_07_21-PM-02_52_32
Last ObjectModification: 2015_02_02-PM-06_40_24

Home Index