nth_of_card_le — Mathlib

English

If hf is a finite set then for any n < |hf.toFinset|, the nth p n equals the image of ⟨n, hn⟩ under the order-embedding of hf.toFinset.

Русский

Если hf является конечным множеством, то при любом n < |hf.toFinset| число nth p n равно образу ⟨n, hn⟩ через отображение порядка hf.toFinset.

LaTeX

$$If hf is finite and n < |hf.toFinset|, then nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩.$$

Lean4

theorem nth_of_card_le (hf : (setOf p).Finite) {n : ℕ} (hn : #hf.toFinset ≤ n) : nth p n = 0 := by
  rw [nth, dif_pos hf, List.getD_eq_default]; rwa [Finset.length_sort]

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