locallyLinear_comap — Mathlib

English

For any equivalence e between α and β and any G on β, the comap of G along e is LocallyLinear if and only if G is LocallyLinear.

Русский

Для любой эквиваленции e между множествами α и β граф G на β будет локально линейным тогда и только тогда, когда граф comap по e из G на α является локально линейным.

LaTeX

$$$(G.{\\rm comap}\\ e).\\text{LocallyLinear} \\iff G.\\text{LocallyLinear}$$$

Lean4

@[simp]
theorem locallyLinear_comap {G : SimpleGraph β} {e : α ≃ β} : (G.comap e).LocallyLinear ↔ G.LocallyLinear :=
  by
  refine ⟨fun h ↦ ?_, ?_⟩
  · rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]
    exact h.map _
  · rw [← Equiv.coe_toEmbedding, ← map_symm]
    exact LocallyLinear.map _

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