Proposition I.3.8 (順序同型は extrema を保存)

• Proposition I.3.8 (順序同型は extrema を保存) #Card
  • 順序同型は上限・下限を保つ。

Back

順序同型 $f$ は extrema を保存する: $$f\left(\bigvee A\right) = \bigvee f(A), \quad f\left(\bigwedge A\right) = \bigwedge f(A)$$ 証明 → 20_Literature/royal_road_to_topology/chapter1

Lean

Notes/ChapterI.lean : prop_I_3_8_sSup / prop_I_3_8_sInf（完備束上、OrderIso.map_sSup/map_sInf を再利用）