bind_defined — Mathlib

English

For any f : Part α and g : α → Part β, for all h ∈ f.Dom, if (g (f.get h)).Dom, then (f.bind g).Dom. This follows from the previous assertion about definedness.

Русский

Для любых f : Part α и g : α → Part β, для всех h ∈ f.Dom, если (g (f.get h)).Dom, то (f.bind g).Dom.

LaTeX

$$$\\forall h:\\, f.Dom,\\ (g (f.get h)).Dom \\Rightarrow (f.bind g).Dom$$$

Lean4

theorem bind_defined {f : Part α} {g : α → Part β} : ∀ h : f.Dom, (g (f.get h)).Dom → (f.bind g).Dom :=
  assert_defined

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