Theorems · Theorem · combinatorics

SimpleGraph.isContained_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.IsContained B ↔ H.IsContained G

If A ≃g H and B ≃g G then A is contained in B if and only if H is contained in G.

Defined in

Mathlib.Combinatorics.SimpleGraph.Copy

Cited by

5 results in Mathlib

Foundations

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