inl_fst_add_inr_snd_eq — Mathlib

English

For any x = (fst, snd) in Unitization R A, we have inl fst + inr snd = x.

Русский

Для любого x = (fst, snd) в Unitization R A имеет место равенство inl fst + inr snd = x.

LaTeX

$$$\\\\forall x : Unitization R A, \\\\mathrm{inl} (x.fst) + (x.snd : Unitization R A) = x.$$$

Lean4

theorem inl_fst_add_inr_snd_eq [AddZeroClass R] [AddZeroClass A] (x : Unitization R A) :
    inl x.fst + (x.snd : Unitization R A) = x :=
  ext (add_zero x.1) (zero_add x.2)

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