two_div_one_sub_two_div_e_le_eight

English

The Behrend sphere image under map(2d−1) is ThreeAPFree.

Русский

Образ сферы Behrend под отображением map(2d−1) является ThreeAPFree.

LaTeX

$$ThreeAPFree\$ ((\\text{sphere } n d k).image (map (2 * d - 1))) : Set ℕ \$ $$

Lean4

theorem two_div_one_sub_two_div_e_le_eight : 2 / (1 - 2 / exp 1) ≤ 8 :=
  by
  rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]
  · linarith [exp_one_gt_d9]
  rw [sub_pos, div_lt_one] <;> exact exp_one_gt_d9.trans' (by norm_num)

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