mono_right

Mathlib.Combinatorics.SimpleGraph.Copy

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mono_right {B' : SimpleGraph β} (h_isub : A ⊑ B) (h_sub : B ≤ B') : A ⊑ B' :=
  h_isub.trans <| IsContained.of_le h_sub

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

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

Разделы

Аффилиация

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