composition (函数复合)
let
define
定义 proposition, 参数
- 单射 := . 记号
- 满射 := . 记号
- 双射 := 单射 and 满射. 记号 . 此时有逆映射
[cardinal]
- . or 存在双射
- . or 存在单射
- . or 存在满射
-
单射和满射的对称
or 存在满射 <==> 存在单射
[cardinal-always-comparable] 元素数量序 的三分 or 序总是 可比较
[finite] := . also let
finite <==>
是有限集 ==> ( 是单射 or 满射 <==> 是双射)
Example 是无限集, 是单射 and 不是满射, so 不是双射
- 可数无限 :=
- [uncountable] 不可数 :=
- [countable] 可数 := i.e. 有限 or 可数无限
保持可数的操作. let , 可数. 以下集合可数
- union: ,
- product: ,
[range] . alias image of , ,
[codomain] . alias range 值域
let
[image] 像
let
[inverse-image] 逆像
==>
逆像
保持
, e.g.
像 只保持 , 对于其它
[cardinal-increase] (cf. cardinal)
不是满射 <==>
find so that
to always have a element in set that not in set , we can define
划分 . 直接 或按照映射 的像集的逆像
[quotient] quotient := or