English
The bottom of the Subgraph lattice is isomorphic to the empty graph on the empty vertex type.
Русский
Нижний элемент решётки подграфов изоморфен пустому графу на пустом множестве вершин.
LaTeX
$$$ (\\perp : Subgraph G).coe \\cong_g emptyGraph Empty $$$
Lean4
/-- The bottom of the `Subgraph G` lattice is isomorphic to the empty graph on the empty
vertex type. -/
def botIso : (⊥ : Subgraph G).coe ≃g emptyGraph Empty
where
toFun v := v.property.elim
invFun v := v.elim
left_inv := fun ⟨_, h⟩ ↦ h.elim
right_inv v := v.elim
map_rel_iff' := Iff.rfl