simpleGraph_trans — Mathlib

English

The simple-graph construction is functorial with respect to composition of equivalences: (e1 ∘ e2).simpleGraph = e1.simpleGraph ∘ e2.simpleGraph.

Русский

Конструкция простого графа функциональна по отношению к композиции эквивалентностей: (e1 ∘ e2).simpleGraph = e1.simpleGraph ∘ e2.simpleGraph.

LaTeX

$$$ (e_1 \\mathrm{trans} e_2).\\mathrm{simpleGraph} = e_1.\\mathrm{simpleGraph}.trans e_2.\\mathrm{simpleGraph} $$$

Lean4

@[simp]
theorem _root_.Equiv.simpleGraph_trans (e₁ : V ≃ W) (e₂ : W ≃ X) :
    (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph :=
  rfl

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