abs_fst_of_mem_pi_polarCoord_target

English

If p lies in the product polarCoord.target, then the first coordinate is nonnegative, so |(p i).1| = (p i).1 for all i.

Русский

Если p принадлежит произведению polarCoord.target, то первая координата неотрицательна, следовательно \|p_i,1\| = p_i,1.

LaTeX

$$$\forall i,\; |(p i)_1| = (p i)_1 \quad (p \in \mathrm{univ.pi}\; \mathrm{polarCoord.target}).$$$

Lean4

theorem abs_fst_of_mem_pi_polarCoord_target {p : ι → ℝ × ℝ} (hp : p ∈ (Set.univ.pi fun _ : ι ↦ polarCoord.target))
    (i : ι) : |(p i).1| = (p i).1 :=
  abs_of_pos ((Set.mem_univ_pi.mp hp) i).1

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