mem_edges_iff — Mathlib

English

If p is Eulerian, then for any edge e, e belongs to p.edges precisely when e belongs to G.edgeSet.

Русский

Если p эйлеров, то для любого ребра e верно: e ∈ p.edges тогда и только тогда, когда e ∈ G.edgeSet.

LaTeX

$$$ p.IsEulerian \Rightarrow \forall e, e \in p.edges \iff e \in G.edgeSet $$$

Lean4

theorem mem_edges_iff {u v : V} {p : G.Walk u v} (h : p.IsEulerian) {e : Sym2 V} : e ∈ p.edges ↔ e ∈ G.edgeSet :=
  ⟨fun h => p.edges_subset_edgeSet h, fun he => by simpa [Nat.succ_le] using (h e he).ge⟩

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