coe_mk — Mathlib

English

The measurable equivalence constructed from an ordinary equivalence e with measurable and measurable inverse has underlying function equal to e.

Русский

Измеримое эквивалентное отображение, построенное из обычного эквивалента e с измеримым отображением и обратным измеримым отображением, имеет подлежащую функцию, равную e.

LaTeX

$$$$ ((\langle e, h_1, h_2 \rangle : \alpha \simeq_m \beta) : \alpha \to \beta) = e. $$$$

Lean4

@[simp]
theorem coe_mk (e : α ≃ β) (h1 : Measurable e) (h2 : Measurable e.symm) : ((⟨e, h1, h2⟩ : α ≃ᵐ β) : α → β) = e :=
  rfl

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