Proposition I.2.1 (同値関係 ↔ 全射)
- Proposition I.2.1 (同値関係 ↔ 全射) #Card
- 空でない $X$ 上の同値関係と全射の対応。
空でない $X$ 上の同値関係全体と、$X$ を定義域とする全射全体の間に全単射対応がある。 同値関係 $\sim$ ↦ 標準全射 $X\to X/\sim$、全射 $f$ ↦ 核 $\ker f$。 証明 → 20_Literature/royal_road_to_topology/chapter1
Notes/ChapterI.lean : prop_I_2_1_ker_mk（Setoid.ker (Quotient.mk r) = r）, prop_I_2_1_quotientEquiv（Quotient (Setoid.ker f) ≃ Y）