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))| Theorem | Name |
| 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] |
| cites the following: | |
| 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] |