bind_defined — Mathlib

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)

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