nth_eq_orderEmbOfFin — Mathlib

English

If hf is finite and n is less than hf.toFinset.card, then nth p n equals the image under the order-embedding of the nth element of hf.toFinset.

Русский

Если hf конечное множество и n < card hf.toFinset, то nth p n равно образу n-го элемента hf.toFinset через отображение порядка.

LaTeX

$$For hf finite, if n < #hf.toFinset, then nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩.$$

Lean4

theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < #hf.toFinset) :
    nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩ := by
  rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_getElem, Fin.getElem_fin]

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