bind₁_comp_bind₁ — Mathlib

English

Composition of bind₁ with itself equals bind₁ of composition: (bind₁ g) ∘ (bind₁ f) = bind₁ (λ i, bind₁ g (f i)).

Русский

Составление bind₁ с самим собой равно 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₁_comp_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → MvPolynomial υ R) :
    (bind₁ g).comp (bind₁ f) = bind₁ fun i => bind₁ g (f i) :=
  by
  ext1
  apply bind₁_bind₁

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