prodEquivOfIsCompl_symm_apply_right

English

For x in q, the symmetric map sends x to (0, x) under prodEquivOfIsCompl; i.e., the right projection is taken to the pair with zero in the first component.

Русский

Для x ∈ q симметрическое отображение отправляет x в (0, x) через prodEquivOfIsCompl; левая компонента ноль.

LaTeX

$$$(prodEquivOfIsCompl p q h).symm x = (0, x)$$$

Lean4

@[simp]
theorem prodEquivOfIsCompl_symm_apply_right (h : IsCompl p q) (x : q) : (prodEquivOfIsCompl p q h).symm x = (0, x) :=
  (prodEquivOfIsCompl p q h).symm_apply_eq.2 <| by simp

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