Theorems · Theorem · combinatorics

SimpleGraph.free_congr

∀ {V : Type u_1} {W : Type u_2} {α : Type u_4} {β : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W}
  {A : SimpleGraph α} {B : SimpleGraph β} (e₁ : A ≃g H) (e₂ : B ≃g G), A.Free B ↔ H.Free G

If A ≃g H and B ≃g G then B is A-free if and only if G is H-free.

Defined in

Mathlib.Combinatorics.SimpleGraph.Copy

Cited by

4 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound