principalSegIio_toRelEmbedding — Mathlib

English

Let α be a preordered set and j an element of α. The principal open segment Iio(j) embeds into α via the natural projection; for any k = (x, hx) in Iio(j), the embedding returns the underlying value x. In other words, the embedding is the projection to the ambient order.

Русский

Пусть α — упорядоченное множество и j — элемент α. Главный открытый сегмент Iio(j) вложен в α естественным образом; для любого k = (x, hx) из Iio(j) вложение возвращает основывающее значение x. Другими словами, вложение есть проекция на внешний порядок.

LaTeX

$$$(\\mathrm{principalSegIio}(j)).\\mathrm{toRelEmbedding}(\\langle x, h_x\\rangle) = x$$$

Lean4

@[simp]
theorem principalSegIio_toRelEmbedding {j : α} (k : Iio j) : (Set.principalSegIio j).toRelEmbedding k = k.1 :=
  rfl

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