toEmbedding_completeGraph — Mathlib

English

The embedding part of the complete graph isomorphism coincides with the standard embedding of the corresponding equivalence.

Русский

Встраиваемая часть изоморфизма между полными графами совпадает со стандартным встраиванием соответствующей эквивалентности.

LaTeX

$$$$ (\\mathrm{Iso.completeGraph}\\, f).toEmbedding = \\mathrm{Embedding.completeGraph}\\; f^{\\mathrm{toEmbedding}} $$$$

Lean4

theorem toEmbedding_completeGraph {α β : Type*} (f : α ≃ β) :
    (Iso.completeGraph f).toEmbedding = Embedding.completeGraph f.toEmbedding :=
  rfl

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