English
If the product a * b has a domain, then the left factor a has a domain.
Русский
Если у произведения a * b существует область определения, то левая составляющая a также определяется.
LaTeX
$$$ (a * b).Dom \Rightarrow a.Dom $$$
Lean4
theorem bind_le {α} (x : Part α) (f : α → Part β) (y : Part β) : x >>= f ≤ y ↔ ∀ a, a ∈ x → f a ≤ y :=
by
constructor <;> intro h
· intro a h' b
have h := h b
simp only [and_imp, bind_eq_bind, mem_bind_iff, exists_imp] at h
apply h _ h'
· intro b h'
simp only [bind_eq_bind, mem_bind_iff] at h'
rcases h' with ⟨a, h₀, h₁⟩
apply h _ h₀ _ h₁
