mk_mem_sparsePairs — Mathlib

English

A pair (u,v) lies in sparsePairs if and only if u,v are parts of P and u ≠ v and their density is below ε.

Русский

Пара (u,v) принадлежит разреженным парам тогда и только тогда, когда u,v — части разбиения, u ≠ v и их плотность меньше ε.

LaTeX

$$((u,v) ∈ P.sparsePairs G ε) ↔ (u ∈ P.parts) ∧ (v ∈ P.parts) ∧ (u ≠ v) ∧ (G.edgeDensity u v < ε)$$

Lean4

@[simp]
theorem mk_mem_sparsePairs (u v : Finset α) (ε : 𝕜) :
    (u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ G.edgeDensity u v < ε := by
  rw [sparsePairs, mem_filter, mem_offDiag, and_assoc, and_assoc]

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