prodEquivOfIsCompl_symm_apply_left

English

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

Русский

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

LaTeX

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

Lean4

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

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