induceUnivIso — Mathlib

English

The graph induced on the whole universe Set.univ is isomorphic to the original graph.

Русский

Граф, индуцируемый на все множество вершин Set.univ, изоморфен исходному графу.

LaTeX

$$$$\\mathrm{induceUnivIso}\\; G\\; :\\; G\\induce\\;\\mathrm{Set.univ} \\;\\cong_g\\; G $$$$

Lean4

/-- The graph induced on `Set.univ` is isomorphic to the original graph. -/
@[simps!]
def induceUnivIso (G : SimpleGraph V) : G.induce Set.univ ≃g G
    where
  toEquiv := Equiv.Set.univ V
  map_rel_iff' := by simp only [Equiv.Set.univ, Equiv.coe_fn_mk, comap_adj, Embedding.coe_subtype, implies_true]

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