coe_finsetOrderIsoSet — Mathlib

English

The underlying function of the order isomorphism between Finset α and Set α is exactly the natural inclusion S ↦ S into α.

Русский

Функция, лежащая в основе порядкового изоморфизма Finset α к Set α, совпадает с естественным включением S ↦ S.

LaTeX

$$$\forall S: Finset\ α,\; (finsetOrderIsoSet)(S)=S$$$

Lean4

@[simp, norm_cast]
theorem coe_finsetOrderIsoSet : ⇑finsetOrderIsoSet = ((↑) : Finset α → Set α) :=
  rfl

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