trans'

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsContained.trans'

English

If B ⊑ C and A ⊑ B then A ⊑ C.

Русский

Если B ⊑ C и A ⊑ B, то A ⊑ C.

LaTeX

$$B ⊑ C → A ⊑ B → A ⊑ C$$

Lean4

/-- If `B` contains `C` and `A` contains `B`, then `A` contains `C`. -/
theorem trans' : B ⊑ C → A ⊑ B → A ⊑ C :=
  flip IsContained.trans

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

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

Разделы

Аффилиация

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