orderEmbeddingOfSet_apply

Mathlib.Order.OrderIsoNat

URI: https://scilib.ai/kg/mathlib#Nat.orderEmbeddingOfSet_apply

English

For any infinite s, the value at n of the order embedding equals the nth element of s.

Русский

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

LaTeX

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

Lean4

theorem orderEmbeddingOfSet_apply [DecidablePred (· ∈ s)] {n : ℕ} : orderEmbeddingOfSet s n = Subtype.ofNat s n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru