coeOrderEmbedding — Mathlib

English

The embedding that sends a two-sided ideal to its underlying set is an order-embedding, i.e., it preserves and reflects inclusion.

Русский

Встраивание, отображающее двусторонний идеал в соответствующее множество, является вложением порядков: включение сохраняется и восстанавливается.

LaTeX

$$TwoSidedIdeal R ↪o Set R$$

Lean4

/-- the coercion from two-sided-ideals to sets is an order embedding
-/
@[simps]
def coeOrderEmbedding : TwoSidedIdeal R ↪o Set R
    where
  toFun := SetLike.coe
  inj' := SetLike.coe_injective
  map_rel_iff' {I J} := ⟨fun (h : (I : Set R) ⊆ (J : Set R)) _ h' ↦ h h', fun h _ h' ↦ h h'⟩

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