coe_IicProdIoc_symm — Mathlib

English

The inverse of the gluing measurable equivalence is the pair (frestrictLe₂ a≤b, restrict₂ Ioc_subset_Iic_self).

Русский

Обратное к склейке — это пара (frestrictLe₂ a≤b, restrict₂ Ioc_subset_Iic_self).

LaTeX

$$$(IicProdIoc(a,b))^{\!-1} = (\mathrm{frestrictLe\_2}(a\le b), \mathrm{restrict\_2} Ioc\_subset\_Iic\_self)$$$

Lean4

theorem coe_IicProdIoc_symm {a b : ι} (hab : a ≤ b) :
    ⇑(IicProdIoc (X := X) hab).symm = fun x ↦ (frestrictLe₂ hab x, restrict₂ Ioc_subset_Iic_self x) :=
  rfl

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