mk_out — Mathlib

English

For any erased element a of α, applying out and then mk yields the original erased element: mk(out(a)) = a.

Русский

Для любого стерто-го элемента a∈Erased α применение out затем mk возвращает исходный элемент: mk(out(a)) = a.

LaTeX

$$$\\mathrm{mk}(\\mathrm{out}(a)) = a$$$

Lean4

@[simp]
theorem mk_out {α} : ∀ a : Erased α, mk (out a) = a
  | ⟨s, h⟩ => by simp only [mk]; congr; exact Classical.choose_spec h

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