measurableEquivRealProd_symm_apply

English

The symm of measuredEquivRealProd applied to p is the pair { re := p.1, im := p.2 }.

Русский

Обратная операция симметрии измеримой эквивалентности RealProd применима к p и возвращает (p.1, p.2).

LaTeX

$$$\text{measurableEquivRealProd.symm}(p) = \{ \text{re} := p_1, \text{im} := p_2 \}$$$

Lean4

@[simp]
theorem measurableEquivRealProd_symm_apply (p : ℝ × ℝ) : measurableEquivRealProd.symm p = { re := p.1, im := p.2 } :=
  rfl

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