card_toFinset_mem_edgeFinset — Mathlib

English

For any edge e of G, the toFinset representation has exactly two elements.

Русский

Для любого ребра e графа G соответствующая toFinset-дляedgeFinset содержит ровно две точки.

LaTeX

$$$(e:\\ Sym^2 V).toFinset.card = 2$$$

Lean4

/-- Mapping an edge to a finite set produces a finset of size `2`. -/
theorem card_toFinset_mem_edgeFinset [DecidableEq V] (e : G.edgeFinset) : (e : Sym2 V).toFinset.card = 2 :=
  Sym2.card_toFinset_of_not_isDiag e.val (G.not_isDiag_of_mem_edgeFinset e.prop)

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