Corollary I.1.6 (グラフと逆関係)
- Corollary I.1.6 (グラフと逆関係) #Card
- グラフであることを逆関係の言葉で。
$F\subset X\times Y$ がグラフ $\iff$ 逆関係 $F^-$ が全射かつ単射。 （I.1.2 の二条件を $F^-$ に翻訳したもの。） 証明 → 20_Literature/royal_road_to_topology/chapter1
Notes/ChapterI.lean : RoyalRoad.ChapterI.cor_I_1_6（RelSurjective/RelInjective）