injOn_pi_polarCoord_symm — Mathlib

English

The map p ↦ polarCoord.symm(p_i) is injective when considered coordinatewise over all i, on the full universal product of targets.

Русский

Координатная карта p ↦ polarCoord.symm(p_i) инъективна при рассмотрении по всем i на произведении целей.

LaTeX

$$$\mathrm{InjOn}\bigl(\lambda p\, (i:\iota) .\; \operatorname{polarCoord.symm}(p i)\bigr)\; (\mathsf{Set.univ}.\mathrm{pi} (\mathrm{polarCoord.target})).$$$

Lean4

theorem injOn_pi_polarCoord_symm :
    Set.InjOn (fun p (i : ι) ↦ polarCoord.symm (p i)) (Set.univ.pi fun _ ↦ polarCoord.target) := fun _ hx _ hy h ↦
  funext fun i ↦ polarCoord.symm.injOn (hx i trivial) (hy i trivial) ((funext_iff.mp h) i)

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