orderIsoShrink_symm_apply — Mathlib

English

For a given a in Shrink(α), the inverse mapping coincides: (orderIsoShrink(α)).symm(a) = (equivShrink(α)).symm(a).

Русский

Для элемента a из Shrink(α) обратное отображение совпадает: (orderIsoShrink(α)).symm(a) = (equivShrink(α)).symm(a).

LaTeX

$$$(\operatorname{orderIsoShrink}(\alpha)).\mathrm{symm}}(a) = (\operatorname{equivShrink}(\alpha)).\mathrm{symm}}(a)$$$

Lean4

@[simp]
theorem orderIsoShrink_symm_apply [Preorder α] (a : Shrink.{u} α) :
    (orderIsoShrink α).symm a = (equivShrink α).symm a :=
  rfl

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