isUniformOfEmpty — Mathlib

English

If a finpartition P of A has no parts, then P is uniform with respect to G at scale ε (the uniformity condition is vacuously satisfied).

Русский

Если разбиение P финитной множества A состоит из нулевых частей, то оно является однородным относительно графа G на масштабе ε (условие однородности выполняется вакуумно).

LaTeX

$$$P.partS = \emptyset \Rightarrow P.IsUniform(G,\varepsilon)$$$

Lean4

theorem isUniformOfEmpty (hP : P.parts = ∅) : P.IsUniform G ε := by simp [IsUniform, hP, nonUniforms]

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