orderEmbeddingOfLTEmbedding_apply

English

The image of an element x under the LT-embedding embedding is the same as applying the original embedding to x.

Русский

Изображение элемента x под LT-вложением совпадает с применением исходного вложения к x.

LaTeX

$$$(\\text{RelEmbedding.instFunLike.coe } f.orderEmbeddingOfLTEmbedding)\\, x = (\\text{RelEmbedding.instFunLike.coe } f)\\, x$.$$

Lean4

@[simp]
theorem orderEmbeddingOfLTEmbedding_apply [PartialOrder α] [PartialOrder β]
    {f : ((· < ·) : α → α → Prop) ↪r ((· < ·) : β → β → Prop)} {x : α} :
    RelEmbedding.orderEmbeddingOfLTEmbedding f x = f x :=
  rfl

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