coe_orderEmbeddingOfSet — Mathlib

English

The underlying function of the order embedding of a set s coincides with mapping n to the nth element of s, viewed as an α-element.

Русский

Функция-образ точки вложения из s совпадает с отображением n на n-ый элемент s, затем рассматриваем как элемент α.

LaTeX

$$$$\mathrm{coe}(\mathrm{Nat.orderEmbeddingOfSet}(s)) = (\mathrm{Subtype.ofNat}(s)).$$$$

Lean4

@[simp]
theorem coe_orderEmbeddingOfSet [DecidablePred (· ∈ s)] : ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s :=
  rfl

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