mem_interedges_iff — Mathlib

English

For any x = (x1, x2), x belongs to the interedges between s and t if and only if x1 ∈ s, x2 ∈ t, and x1 is adjacent to x2 in G.

Русский

Для любого x = (x1, x2) выполняется: x ∈ G.interedges(s, t) тогда и только тогда, когда x1 ∈ s, x2 ∈ t и x1 смежно x2 в графе G.

LaTeX

$$$x \in G.interedges(s,t) \iff x.1 \in s \wedge x.2 \in t \wedge G.Adj x.1 x.2$$$

Lean4

theorem mem_interedges_iff {x : α × α} : x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2 :=
  Rel.mem_interedges_iff

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