isUniform_one — Mathlib

English

A partition is 1-uniform for any graph: density is preserved at scale 1.

Русский

Разбиение является 1-однородным для любого графа: плотности сохраняются на масштабе 1.

LaTeX

$$$G.IsUniform(1,s,t)$$$

Lean4

theorem isUniform_one : G.IsUniform (1 : 𝕜) s t :=
  by
  intro s' hs' t' ht' hs ht
  rw [mul_one] at hs ht
  rw [eq_of_subset_of_card_le hs' (Nat.cast_le.1 hs), eq_of_subset_of_card_le ht' (Nat.cast_le.1 ht), sub_self,
    abs_zero]
  exact zero_lt_one

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