leftInverse_comap_map — Mathlib

English

The pair (comap f, map f) forms a left inverse: LeftInverse (SimpleGraph.comap f) (SimpleGraph.map f).

Русский

Пара (comap f, map f) образует левую обратную связь: LeftInverse (SimpleGraph.comap f) (SimpleGraph.map f).

LaTeX

$$$$ \\text{LeftInverse}(\\mathrm{SimpleGraph.comap} f, \\mathrm{SimpleGraph.map} f) $$$$

Lean4

theorem leftInverse_comap_map (f : V ↪ W) : Function.LeftInverse (SimpleGraph.comap f) (SimpleGraph.map f) :=
  comap_map_eq f

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