English
If p ⊆ f.Dom and ∀ x, p ⊆ (g x).Dom, then p ⊆ (f >>= g).Dom.
Русский
Если p ⊆ Dom f и для каждого x выполняется p ⊆ Dom (g x), тогда p ⊆ Dom (f >>= g).
LaTeX
$$$p \\subseteq \\mathrm{Dom}(f) \\quad\\text{and}\\quad \\forall x,\\; p \\subseteq \\mathrm{Dom}(g(x)) \\Rightarrow p \\subseteq \\mathrm{Dom}(\\mathrm{monad}.bind f g).Dom$$$
Lean4
theorem bind_defined {α β γ} (p : Set α) {f : α →. β} {g : β → α →. γ} (H1 : p ⊆ f.Dom) (H2 : ∀ x, p ⊆ (g x).Dom) :
p ⊆ (f >>= g).Dom := fun a ha => (⟨H1 ha, H2 _ ha⟩ : (f >>= g).Dom a)