coe_coe — Mathlib

English

The underlying function of a trivialization coincides with its representation as an open partial homeomorphism.

Русский

Базовая функция тривиализации совпадает с её представлением как открытого частичного гомоморфизма.

LaTeX

$$$\big(\mathrm{toOpenPartialHomeomorph}(e)\big) = e\quad \text{as functions}$$$

Lean4

@[simp, mfld_simps]
theorem coe_coe : ⇑e.toOpenPartialHomeomorph = e :=
  rfl

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