botIso — Mathlib

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

Похожие утверждения