verts_monotone

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.verts_monotone

English

The function that assigns to a subgraph its vertex set is monotone.

Русский

Функция, сопоставляющая подграфу его множество вершин, монотонна.

LaTeX

$$$ \\text{Monotone} (\\mathrm{verts} : G.Subgraph \\to Set V) $$$

Lean4

theorem verts_monotone : Monotone (verts : G.Subgraph → Set V) := fun _ _ h ↦ h.1

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

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

Разделы

Аффилиация

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