mono_left

Mathlib.Combinatorics.SimpleGraph.Copy

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

English

If A ≤ A' and A' ⊑ B then A ⊑ B.

Русский

Если A ≤ A' и A' ⊑ B, то A ⊑ B.

LaTeX

$$A ≤ A' → A' ⊑ B → A ⊑ B$$

Lean4

theorem mono_left {A' : SimpleGraph α} (h_sub : A ≤ A') (h_isub : A' ⊑ B) : A ⊑ B :=
  (IsContained.of_le h_sub).trans h_isub

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

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

Разделы

Аффилиация

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