fintypeEdgeSetSup — Mathlib

English

If V has a decidable equality and both G1 and G2 have finite edge sets, then the edge set of the supremum G1 ⊔ G2 is finite.

Русский

Если для множества вершин V задано разрешимое равенство и графы G1 и G2 имеют конечные множества рёбер, то множество рёбер графа верхнего объединения G1 ⊔ G2 конечно.

LaTeX

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

Lean4

instance fintypeEdgeSetSup [DecidableEq V] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] : Fintype (G₁ ⊔ G₂).edgeSet :=
  by
  rw [edgeSet_sup]
  infer_instance

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