opOrderIso — Mathlib

English

TwoSidedIdeal R and TwoSidedIdeal R^{op} are in bijective, order-preserving correspondence.

Русский

Двусторонние идеалы R и R^{op} существуют в биективной, сохраняющей порядок корреспонденции.

LaTeX

$$opOrderIso : TwoSidedIdeal R \cong_o TwoSidedIdeal R^{op}$$

Lean4

/-- Two-sided-ideals of `A` and that of `Aᵒᵖ` corresponds bijectively to each other.
-/
@[simps]
def opOrderIso : TwoSidedIdeal R ≃o TwoSidedIdeal Rᵐᵒᵖ
    where
  toFun := op
  invFun := unop
  map_rel_iff' {I' J'} := by simpa [ringCon_le_iff] using RingCon.opOrderIso.map_rel_iff

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