apply — Mathlib

English

The coercion of a bijective CoalgEquiv to a function is bijective as a function.

Русский

Приведение коалгебраической эквивалентности к функции сохраняет биективность как функция.

LaTeX

$$$\\text{coe\_ofBijective} : (hf : \\mathbf{Bijective} (CoalgHom.funLike.coe f)) \\Rightarrow \\mathrm{Bijective} (\\mathrm{CoalgHom.funLike.coe} f)$$$

Lean4

/-- See Note [custom simps projection] -/
def apply {R α β : Type*} [CommSemiring R] [AddCommMonoid α] [Module R α] [AddCommMonoid β] [Module R β]
    [CoalgebraStruct R α] [CoalgebraStruct R β] (f : α →ₗc[R] β) : α → β :=
  f

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