coeSubgraph_injective — Mathlib

English

The map Subgraph.coeSubgraph is injective; i.e., different G'.coe.Subgraph map to different Subgraphs of G.

Русский

Отображение Subgraph.coeSubgraph инъективно: разные G'.coe.Subgraph приводят к различным подграфам G.

LaTeX

$$$\\text{Subgraph.coeSubgraph}$ is injective;\\, \\mathrm{Injective}(\\mathrm{Subgraph.coeSubgraph})$$$

Lean4

theorem coeSubgraph_injective (G' : G.Subgraph) :
    Function.Injective (Subgraph.coeSubgraph : G'.coe.Subgraph → G.Subgraph) :=
  Function.LeftInverse.injective restrict_coeSubgraph

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