hundred_div_ε_pow_five_le_m — Mathlib

English

A bound involving 100 divided by ε^5 is at most m.

Русский

Соотношение 100 / ε^5 ≤ m выполняется под условия.

LaTeX

$$100 / ε^5 ≤ m$$

Lean4

theorem hundred_div_ε_pow_five_le_m [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α)
    (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) : 100 / ε ^ 5 ≤ m :=
  (div_le_of_le_mul₀ (eps_pow_five_pos hPε).le (by positivity) hPε).trans <|
    by
    norm_cast
    rwa [Nat.le_div_iff_mul_le (stepBound_pos (P.parts_nonempty <| univ_nonempty.ne_empty).card_pos), stepBound,
      mul_left_comm, ← mul_pow]

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