coe_finsetOrderIsoSet_symm — Mathlib

English

The inverse of the finite-set to set order isomorphism corresponds to the inverse of the canonical finite-set to set equivalence.

Русский

Обратное отображение между Finset α и Set α совпадает с обратным отображением обычного эквивалента между этими множествами.

LaTeX

$$$(finsetOrderIsoSet)^{-1} = (finsetEquivSet)^{-1}$$$

Lean4

@[simp]
theorem coe_finsetOrderIsoSet_symm : ⇑(finsetOrderIsoSet : Finset α ≃o Set α).symm = ⇑finsetEquivSet.symm :=
  rfl

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