nth_eq_orderIsoOfNat — Mathlib

English

If hf is infinite, then nth p equals the composition of the coercion with Nat.Subtype.orderIsoOfNat (setOf p).

Русский

Если hf бесконечно, тогда nth p эквивалентно композиции отображения сопряжения со Nat.Subtype.orderIsoOfNat (setOf p).

LaTeX

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

Lean4

/-- When `s` is an infinite set, `nth` agrees with `Nat.Subtype.orderIsoOfNat`. -/
theorem nth_eq_orderIsoOfNat (hf : (setOf p).Infinite) :
    nth p = (↑) ∘ @Nat.Subtype.orderIsoOfNat (setOf p) hf.to_subtype :=
  funext <| nth_apply_eq_orderIsoOfNat hf

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