comap_surjective

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.comap_surjective

English

The comap by any embedding f is surjective: Function.Surjective (SimpleGraph.comap f).

Русский

Комап по любому вложению f сюръективно: Function.Surjective (SimpleGraph.comap f).

LaTeX

$$$$ \\text{Surjective}(\\mathrm{SimpleGraph.comap} f) $$$$

Lean4

theorem comap_surjective (f : V ↪ W) : Function.Surjective (SimpleGraph.comap f) :=
  (leftInverse_comap_map f).surjective

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

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

Разделы

Аффилиация

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