orderEmbeddingOfInjective — Mathlib

English

We can regard an injective map preserving binary infima as an order embedding.

Русский

Инъективное отображение, сохраняющее бинарные инфимы, является вложением по порядку.

LaTeX

$$$$ \text{orderEmbeddingOfInjective}(f,hf) : \alpha \hookrightarrow_o \beta. $$$$

Lean4

/-- We can regard an injective map preserving binary infima as an order embedding. -/
@[simps! apply]
def orderEmbeddingOfInjective [SemilatticeInf α] [SemilatticeInf β] (f : F) [InfHomClass F α β] (hf : Injective f) :
    α ↪o β :=
  OrderEmbedding.ofMapLEIff f
    (fun x y ↦ by
      refine ⟨fun h ↦ ?_, fun h ↦ OrderHomClass.mono f h⟩
      rwa [← inf_eq_left, ← hf.eq_iff, map_inf, inf_eq_left])

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