recolorOfEquiv — Mathlib

English

Given an equivalence f: α ≃ β, there is an induced equivalence between colorings: G.Coloring α ≃ G.Coloring β.

Русский

Дано эквивалентность f: α ≃ β, существует индуцированная эквивалентность раскрасок: G.Coloring α ≃ G.Coloring β.

LaTeX

$$$\\text{recolorOfEquiv } f : G.Coloring α \\simeq G.Coloring β$$$

Lean4

/-- Given an equivalence, there is an induced equivalence between colorings. -/
def recolorOfEquiv {α β : Type*} (f : α ≃ β) : G.Coloring α ≃ G.Coloring β
    where
  toFun := G.recolorOfEmbedding f.toEmbedding
  invFun := G.recolorOfEmbedding f.symm.toEmbedding
  left_inv
    C := by
    ext v
    apply Equiv.symm_apply_apply
  right_inv
    C := by
    ext v
    apply Equiv.apply_symm_apply

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