instFintype — Mathlib

English

If G has a finite edge set, then the edge set of G.killCopies(H) is finite.

Русский

Если множество ребер G конечно, тогда множество ребер G.killCopies(H) конечно.

LaTeX

$$$ Fintype G.edgeSet \Rightarrow Fintype (G.killCopies H).edgeSet $$$

Lean4

noncomputable instance instFintype : Fintype (G.killCopies H).edgeSet :=
  .ofInjective (Set.inclusion <| edgeSet_mono killCopies_le_left) <| Set.inclusion_injective _

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