orderIsoOfNat_apply — Mathlib

English

For any infinite s, the nth value of the order isomorphism equals the nth element of s.

Русский

Для бесконечного s n-ое значение изоморфизма порядка равно n-ому элементу s.

LaTeX

$$$$\mathrm{Nat.Subtype.orderIsoOfNat}(s)(n) = \mathrm{Nat.Subtype.ofNat}(s)(n).$$$$

Lean4

@[simp]
theorem orderIsoOfNat_apply [dP : DecidablePred (· ∈ s)] {n : ℕ} : Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by
  simp [orderIsoOfNat]; congr!

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