coe_trans — Mathlib

English

The underlying function of the composite f.trans g equals the composition of the underlying functions: (f.trans g : α → γ) = g ∘ f.

Русский

Лежащая в основе функция композиции f.trans g равна композиции функций f и g: (f.trans g : α → γ) = g ∘ f.

LaTeX

$$$(f.trans g : α \to γ) = g \circ f$.$$

Lean4

@[to_additive (attr := simp)]
theorem coe_trans (f : α ≃*o β) (g : β ≃*o γ) : (f.trans g : α → γ) = g ∘ f :=
  rfl

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