free_congr

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.free_congr

← MathLib Explorer

English

If A ≃g H and B ≃g G then A.Free B ↔ G.Free H.

Русский

Если A ≃g H и B ≃g G, то A.Free B эквивалентно G.Free H.

LaTeX

$$A \cong_g H ∧ B \cong_g G ⇒ (A.Free B ↔ G.Free H)$$

Lean4

/-- If `A ≃g H` and `B ≃g G` then `B` is `A`-free if and only if `G` is `H`-free. -/
theorem free_congr (e₁ : A ≃g H) (e₂ : B ≃g G) : A.Free B ↔ H.Free G :=
  (isContained_congr e₁ e₂).not

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru