orderEmbeddingOfSet_range

Mathlib.Order.OrderIsoNat

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

English

The range of the order embedding of s equals s.

Русский

Образ вложения порядка from s равен s.

LaTeX

$$$$\mathrm{Set.range}(\mathrm{Nat.orderEmbeddingOfSet}(s)) = s.$$$$

Lean4

theorem orderEmbeddingOfSet_range [DecidablePred (· ∈ s)] : Set.range (Nat.orderEmbeddingOfSet s) = s :=
  Subtype.coe_comp_ofNat_range

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

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

Разделы

Аффилиация

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