think_empty — Mathlib

English

Let α be a type. The distinguished element empty α of Computation α satisfies the fixed-point identity empty α = think (empty α).

Русский

Пусть α — множество. Вычисление empty α в Computation α удовлетворяет тождеству fixed-point операции think: empty α = think (empty α).

LaTeX

$$$empty_{\alpha} = \mathrm{think}(empty_{\alpha})$$$

Lean4

theorem think_empty : empty α = think (empty α) :=
  destruct_eq_think destruct_empty

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