bind₁_bind₁ — Mathlib

English

Monadic associativity for bind₁: (bind₁ g) ∘ (bind₁ f) = bind₁ (λ i, bind₁ g (f i)) and φ is arbitrary polynomial.

Русский

Ассоциативность монады для bind₁: (bind₁ g) ∘ (bind₁ f) = bind₁ (λ i, bind₁ g (f i)) для произвольного φ.

LaTeX

$$$(\text{bind}_1 g) \circ (\text{bind}_1 f) = \text{bind}_1 (\lambda i. \text{bind}_1 g (f i))$$$

Lean4

theorem bind₁_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R) (φ : MvPolynomial σ R) :
    (bind₁ g) (bind₁ f φ) = bind₁ (fun i => bind₁ g (f i)) φ := by simp [bind₁, ← comp_aeval]

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