of_bind — Mathlib

English

Let a be a partial element of α and f: α → Part β. If a.bind f is defined (has a Dom), then a is defined.

Русский

Пусть a — частичный элемент типа α и f : α → Part β. Если (a.bind f) определён (имеет домен), то a определён.

LaTeX

$$$\operatorname{Dom}(a \bind f) \rightarrow \operatorname{Dom}(a)$$$

Lean4

theorem of_bind {f : α → Part β} {a : Part α} (h : (a.bind f).Dom) : a.Dom :=
  h.1

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