coe_coeHom — Mathlib

English

The coercion from NonemptyInterval to Set α coincides with the canonical coeHom embedding; they are equal as functions.

Русский

Строгий переход от NonemptyInterval к Set α совпадает с каноническим вложением coeHom; это одинаковые функции.

LaTeX

$$$ (coeHom : NonemptyInterval α → Set α) = (↑) : NonemptyInterval α → Set α $$$

Lean4

@[simp]
theorem coe_coeHom : (coeHom : NonemptyInterval α → Set α) = ((↑) : NonemptyInterval α → Set α) :=
  rfl

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