coe_prodEquivOfIsCompl' — Mathlib

English

The symmetric application of prodEquivOfIsCompl to a pair maps back to a sum representation with the left component 0 or right component 0 depending on the side; i.e., symmetry yields (0, x) or (x, 0) accordingly.

Русский

Симметрическое применение prodEquivOfIsCompl к паре восстанавливает сумму: либо (0, x), либо (x, 0) в зависимости от стороны.

LaTeX

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

Lean4

@[simp]
theorem coe_prodEquivOfIsCompl' (h : IsCompl p q) (x : p × q) : prodEquivOfIsCompl p q h x = x.1 + x.2 :=
  rfl

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