coe_IicProdIoc — Mathlib

English

The canonical coe map of the measurable equivalence MeasurableEquiv.IicProdIoc is exactly the underlying gluing IicProdIoc on the index structure.

Русский

Каноническое отображение приводится к базовой функции-склейке IicProdIoc.

LaTeX

$$$\big( \mathrm{MeasurableEquiv}.IicProdIoc(a,b) \big) = \mathrm{IicProdIoc}(a,b)$$$

Lean4

theorem coe_IicProdIoc {a b : ι} (hab : a ≤ b) : ⇑(IicProdIoc (X := X) hab) = _root_.IicProdIoc a b :=
  rfl

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