toLawson_ofLawson — Mathlib

English

For every a in WithLawson α, the composition toLawson ∘ ofLawson is the identity on WithLawson α; i.e., toLawson (ofLawson a) = a.

Русский

Для каждого a из WithLawson α композиция toLawson ∘ ofLawson равна тождественности на WithLawson α; то есть toLawson(ofLawson(a)) = a.

LaTeX

$$$\mathrm{toLawson}(\mathrm{ofLawson}(a)) = a$ for all $a$ in $\mathrm{WithLawson}(\alpha)$$$

Lean4

@[simp]
theorem toLawson_ofLawson (a : WithLawson α) : toLawson (ofLawson a) = a :=
  rfl

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