P:(
Prop).
Thm* (
a:, b:{...a}. P(a,b))
Thm*
Thm* (
a:, b:{a+1...}. (c:{a..b
}. P(a,c)) P(a,b)) (a,b:. P(a,b))P:(Prop), a:.
Thm* (
b:{...a}. P(a,b))
Thm*
Thm* (
b:{a+1...}. (c:{a..b}. P(a,c)) P(a,b)) (b:. P(a,b))is mentioned by
| P:(Prop).
Thm* ( a:, b:{...a}. P(a,b))
Thm*
Thm* ( a:, b:{a+1...}. (c:{a..b}. P(a,c)) P(a,b)) (a,b:. P(a,b)) | [all_int_segs_by_upper_ind] |
| P:(Prop), a:.
Thm* ( b:{...a}. P(a,b))
Thm*
Thm* ( b:{a+1...}. (c:{a..b}. P(a,c)) P(a,b)) (b:. P(a,b)) | [int_segs_from_base_by_upper_ind] |
In prior sections: core well fnd int 1 bool 1 rel 1 LogicSupplement int 2 num thy 1
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html