i:
, j:{i...}. WellFnd{u}({i..j
};x,y.x>y)r:(A
AProp), B:Type, f:(BA).
Thm* WellFnd{i}(A;x,y.r(x,y))
WellFnd{i}(B;x,y.r(f(x),f(y)))n:. WellFnd{i}({n...};x,y.x<y)| Rank | Theorem | Name |
| 4 | i:, j:{i...}. WellFnd{u}({i..j};x,y.x>y) | [int_seg_well_founded_down] |
| cites the following: | ||
| 1 | r:(AAProp), B:Type, f:(BA).
Thm* WellFnd{i}(A;x,y.r(x,y)) WellFnd{i}(B;x,y.r(f(x),f(y))) | [inv_image_ind] |
| 3 | n:. WellFnd{i}({n...};x,y.x<y) | [int_upper_well_founded] |