not_adj_iff_part_eq — Mathlib

English

Two vertices are not adjacent if and only if they lie in the same partition class of the Turán finpartition.

Русский

Две вершины не смежны тогда и только тогда, когда они принадлежат одному классу разбиения финпартиции Турэна.

LaTeX

$$$\neg G.\mathrm{Adj} \;s \;t \iff h.finpartition.part s = h.finpartition.part t.$$$

Lean4

theorem not_adj_iff_part_eq [DecidableEq V] : ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t :=
  by
  change h.setoid.r s t ↔ _
  rw [← Finpartition.mem_part_ofSetoid_iff_rel]
  let fp := h.finpartition
  change t ∈ fp.part s ↔ fp.part s = fp.part t
  rw [fp.mem_part_iff_part_eq_part (mem_univ t) (mem_univ s), eq_comm]

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