fintypeEdgeSetSdiff — Mathlib

English

If G1 and G2 have finite edge sets, then the edge set of G1 \\ G2 is finite.

Русский

Если графы G1 и G2 имеют конечные множества рёбер, то множество рёбер графа G1 \\ G2 конечно.

LaTeX

$$$\\operatorname{Fintype}( (G_1 \\ G_2).\\mathrm{edgeSet} )$$$

Lean4

instance fintypeEdgeSetSdiff [DecidableEq V] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] : Fintype (G₁ \ G₂).edgeSet :=
  by
  rw [edgeSet_sdiff]
  exact Set.fintypeDiff _ _

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