nth_apply_eq_orderIsoOfNat — Mathlib

English

If hf is infinite, then nth p n equals the order isomorphism of the set {k | p(k)} applied to n.

Русский

Если множество p бесконечно, тогда nth p n эквивалентно применению отображения упорядочивания к множеству {k | p(k)} к аргументу n.

LaTeX

$$nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n$$

Lean4

/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`. -/
theorem nth_apply_eq_orderIsoOfNat (hf : (setOf p).Infinite) (n : ℕ) :
    nth p n = @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype n := by rw [nth, dif_neg hf]

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