sphere_subset_preimage_metric_sphere

English

Let f be the map x \\mapsto ToLp_2((↑) ∘ x). Then every x in Behrend's sphere n d k lies in the preimage under f of the metric sphere centered at 0 with radius √k.

Русский

Пусть f(x) = ToLp_2((↑) ∘ x). Тогда каждый элемент x из сферы Behrend с параметрами n d k принадлежит предобразу подмножества метрического шара с центром в нуле и радиусом √k.

LaTeX

$$$ x\\in sphere\\, n\\, d\\, k \\Rightarrow f(x) \\in Metric.sphere(0,\\sqrt{k}) $ where $ f(x)=ToLp_2((↑) \\circ x) $$$

Lean4

theorem sphere_subset_preimage_metric_sphere :
    (sphere n d k : Set (Fin n → ℕ)) ⊆
      (fun x : Fin n → ℕ => WithLp.toLp 2 ((↑) ∘ x : Fin n → ℝ)) ⁻¹'
        Metric.sphere (0 : PiLp 2 fun _ : Fin n => ℝ) (√↑k) :=
  fun x hx => by rw [Set.mem_preimage, mem_sphere_zero_iff_norm, norm_of_mem_sphere hx]

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