toOrderEmbedding_apply

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#InitialSeg.toOrderEmbedding_apply

English

For an initial segment embedding f, applying the obtained order embedding to x yields f(x).

Русский

Для отображения InitialSeg f, применение полученного вложения порядка к x дает f(x).

LaTeX

$$$f^{toOrderEmbedding}(x) = f(x).$$$

Lean4

@[simp]
theorem toOrderEmbedding_apply [PartialOrder α] [PartialOrder β] (f : α ≤i β) (x : α) : f.toOrderEmbedding x = f x :=
  rfl

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

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

Разделы

Аффилиация

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