isContained_congr_left

Mathlib.Combinatorics.SimpleGraph.Copy

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

English

If e₁ : A ≃g B, then A ⊑ C iff B ⊑ C.

Русский

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

LaTeX

$$e₁ : A ≃g B → (A ⊑ C ↔ B ⊑ C)$$

Lean4

theorem isContained_congr_left (e₁ : A ≃g B) : A ⊑ C ↔ B ⊑ C :=
  isContained_congr e₁ .refl

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

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

Разделы

Аффилиация

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