Nuprl - DiscreteMath Citations of cand

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def A & B == A

is mentioned by

Thm*  (A Discrete)
Thm*
Thm*  (k:, f:(k inj A).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Bij(k; {a:A| i:k. a = f(i) }; f)) [nsub_inj_discr_range_bij]

Thm*  (A Discrete)
Thm*
Thm*  (k:, f:(kA).
Thm*  ({a:A| i:k. a = f(i) }  Type
Thm*  (& f  k{a:A| i:k. a = f(i) }
Thm*  (& Surj(k; {a:A| i:k. a = f(i) }; f)) [nsub_discr_range_surj]

Thm*  Inj({u:| P(u) }; {v:| Q(v) }; f)
Thm*
Thm*  (m:{u:| P(u) }, k:{v:| Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:| P(u) & u = m }{v:| Q(v) & v = k }
Thm*  (& Inj({u:| P(u) & u = m }; {v:| Q(v) & v = k };
Thm*  (& Inj(Replace value k by f(m) in f)) [delete_fenum_value_is_inj_genW]

In prior sections: LogicSupplement

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

DiscreteMath Sections DiscrMathExt Doc

Thm* (A Discrete) Thm* Thm* (k:, f:(k inj A). Thm* ({a:A\| i:k. a = f(i) } Type Thm* (& f k{a:A\| i:k. a = f(i) } Thm* (& Bij(k; {a:A\| i:k. a = f(i) }; f))	[nsub_inj_discr_range_bij]
Thm* (A Discrete) Thm* Thm* (k:, f:(kA). Thm* ({a:A\| i:k. a = f(i) } Type Thm* (& f k{a:A\| i:k. a = f(i) } Thm* (& Surj(k; {a:A\| i:k. a = f(i) }; f))	[nsub_discr_range_surj]
Thm* Inj({u:\| P(u) }; {v:\| Q(v) }; f) Thm* Thm* (m:{u:\| P(u) }, k:{v:\| Q(v) }. Thm* ((Replace value k by f(m) in f) Thm* ( {u:\| P(u) & u = m }{v:\| Q(v) & v = k } Thm* (& Inj({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Thm* (& Inj(Replace value k by f(m) in f))	[delete_fenum_value_is_inj_genW]