mk_mem_nonUniforms — Mathlib

English

The bottom Finpartition has empty nonUniforms set for ε > 0, i.e., there are no nonuniform pairs there.

Русский

Нижнее разбиение имеет пустой набор неоднородных пар для ε > 0.

LaTeX

$$(⊥ : Finpartition A).nonUniforms G ε = ∅$$

Lean4

@[simp]
theorem mk_mem_nonUniforms : (u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v := by
  rw [nonUniforms, mem_filter, mem_offDiag, and_assoc, and_assoc]

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