free_congr_right

Mathlib.Combinatorics.SimpleGraph.Copy

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

English

If e₂ : B ≃g C, then A.Free B ↔ A.Free C.

Русский

Если e₂: B ≃g C, то A.Free B эквивалентно A.Free C.

LaTeX

$$e₂ : B ≃g C → (A.Free B ↔ A.Free C)$$

Lean4

theorem free_congr_right (e₂ : B ≃g C) : A.Free B ↔ A.Free C :=
  free_congr .refl e₂

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

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

Разделы

Аффилиация

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