pow_mul_m_le_card_part — Mathlib

English

If P is an equipartition and u is a part of P, then 4^{|P.parts|} · m ≤ |u|.

Русский

Если P — равномерное разбиение, и u — часть этого разбиения, то 4^{|P.parts|} · m ≤ |u|.

LaTeX

$$$4^{|P.parts|} \cdot m \le |u|$$$

Lean4

theorem pow_mul_m_le_card_part (hP : P.IsEquipartition) (hu : u ∈ P.parts) : (4 : ℝ) ^ #P.parts * m ≤ #u :=
  by
  norm_cast
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  exact (Nat.mul_div_le _ _).trans (hP.average_le_card_part hu)

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