surjective — Mathlib

English

The map sending a vertex of a matching to its incident edge is surjective onto the edge set.

Русский

Отображение вершины соответствия на инцидентное ребро отображает всю множества ребер.

LaTeX

$$$$\\text{Surjective } h.toEdge$$$$

Lean4

theorem surjective (h : M.IsMatching) : Surjective h.toEdge :=
  by
  rintro ⟨⟨x, y⟩, he⟩
  exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj _ he⟩

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