bot_isUniform — Mathlib

English

If a partition P is ε-uniform and ε ≤ ε', then P is ε'-uniform.

Русский

Если разбиение P ε-однородно и ε ≤ ε', то P ε'-однородно.

LaTeX

$$P.IsUniform G ε ∧ ε ≤ ε' ⇒ P.IsUniform G ε'$$

Lean4

theorem bot_isUniform (hε : 0 < ε) : (⊥ : Finpartition A).IsUniform G ε :=
  by
  rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty, Nat.cast_zero]
  exact mul_nonneg (Nat.cast_nonneg _) hε.le

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