| Who Cites same range sep? |
|
same_range_sep | Def same_range_sep(A; B) ==  f,g. j:B. ( i:A. f(i) = j)  ( i:A. g(i) = j) |
|
| Thm* same_range_sep(A; B) (A B) (A B) Prop |
|
| Thm* same_range_sep(A; B) (A inj B) (A inj B) Prop |
|
iff | Def P  Q == (P  Q) & (P  Q) |
|
| Thm* A,B:Prop. (A  B) Prop |
|
so_lambda2 | Def ( 1,2. b(1;2))(1,2) == b(1;2) |
|
rev_implies | Def P  Q == Q  P |
|
| Thm* A,B:Prop. (A  B) Prop |