coe_orderIsoOfFin_apply — Mathlib

English

The coercion of the order isomorphism equals the corresponding finite order embedding on any index i.

Русский

Предел преобразования изоморфизма порядка равен соответствующему вложению по порядку на любом индексе i.

LaTeX

$$$ \\uparrow(\\operatorname{orderIsoOfFin}(s,h)(i)) = \\operatorname{orderEmbOfFin}(s,h)(i) $$$

Lean4

@[simp]
theorem coe_orderIsoOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) :
    ↑(orderIsoOfFin s h i) = orderEmbOfFin s h i :=
  rfl

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