i,j:
, F:({i..j
}
Prop).
(k:{i..j}. Dec(F(k))) 
Dec(k:{i..j}. F(k))i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(
k:{i..j}. F(k))| Rank | Theorem | Name |
| 7 |
Thm* i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__all_int_seg] |
| cites | ||
| 6 |
Thm* i,j:, F:({i..j}Prop).
(k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k)) | [decidable__ex_int_seg] |