mem_incidenceFinset — Mathlib

English

An incidence e belongs to the Finset incidenceFinset v iff e belongs to the incidenceSet v.

Русский

Элемент-инцидент e принадлежит Finset incidenceFinset v тогда и только тогда, когда он принадлежит incidenceSet v.

LaTeX

$$$ e \in G.incidenceFinset v \iff e \in G.incidenceSet v $$$

Lean4

@[simp]
theorem mem_incidenceFinset [DecidableEq V] (e : Sym2 V) : e ∈ G.incidenceFinset v ↔ e ∈ G.incidenceSet v :=
  Set.mem_toFinset

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