dart_fst_fiber — Mathlib

English

If V is finite and G.Adj is decidable, then G.Dart is finite.

Русский

Если V конечен и G.Adj разрешим, то G.Dart конечен.

LaTeX

$$$ Fintype G.Dart $$$

Lean4

theorem dart_fst_fiber [DecidableEq V] (v : V) :
    ({d : G.Dart | d.fst = v} : Finset _) = univ.image (G.dartOfNeighborSet v) :=
  by
  ext d
  simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]
  constructor
  · rintro rfl
    exact ⟨_, d.adj, by ext <;> rfl⟩
  · rintro ⟨e, he, rfl⟩
    rfl

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