coe_mul — Mathlib

English

Let e1 and e2 be isometric bijections from a metric space to itself. Then their multiplication corresponds to ordinary composition: e1 * e2 = e1 ∘ e2.

Русский

Пусть e1 и e2 — изометрические биективные отображения пространства на себя. Тогда произведение e1 * e2 соответствует обычной композиции: e1 * e2 = e1 ∘ e2.

LaTeX

$$$ (e_1 * e_2) = e_1 \circ e_2 $$$

Lean4

@[simp]
theorem coe_mul (e₁ e₂ : α ≃ᵢ α) : ⇑(e₁ * e₂) = e₁ ∘ e₂ :=
  rfl

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