coe_toEquiv — Mathlib

English

The map toEquiv is compatible with the mk constructor in the sense that the coe of the constructed uniform equivalence equals the given equivalence.

Русский

Отображение toEquiv совместимо с конструктором mk: коe сконструированного UniformEquiv совпадает с данным эквивалентом.

LaTeX

$$$(UniformEquiv.mk a b c).toEquiv = a$$$

Lean4

@[simp]
theorem coe_toEquiv (h : α ≃ᵤ β) : ⇑h.toEquiv = h :=
  rfl

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