Proposition I.1.2 (グラフ判定)
- Proposition I.1.2 (グラフ判定) #Card
- 関係 $F\subset X\times Y$ がグラフであるための必要十分条件。
$F$ がグラフ $\iff$ 全域性 $F^- Y = X$ かつ 一価性 $F^- y_0 \cap F^- y_1 \neq \emptyset \implies y_0 = y_1$。 証明 → 20_Literature/royal_road_to_topology/chapter1
Notes/ChapterI.lean : RoyalRoad.ChapterI.prop_I_1_2（IsGraph F := ∀ x, ∃! y, (x,y) ∈ F）