mk_get — Mathlib

English

The map comp.mk is a left-inverse of comp.get; composing mk after get yields the original element.

Русский

Мапа comp.mk является левой обратной comp.get; композиция mk после get возвращает исходный элемент.

LaTeX

$$$\\operatorname{comp.mk}\\bigl( \\operatorname{comp.get} x \\bigr) = x$$$

Lean4

@[simp]
theorem mk_get (x : comp P Q α) : comp.mk (comp.get x) = x := by
  rfl
    /-
    lifting predicates and relations
    -/

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