map_monotone

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

The map operation is monotone with respect to inclusion.

Русский

Операция отображения монотонна по включению.

LaTeX

$$$ \text{Monotone}(\\text{Subgraph.map } f) $$$

Lean4

theorem map_monotone : Monotone (Subgraph.map f) := fun _ _ ↦ map_mono

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

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

Разделы

Аффилиация

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