instLinearOrderIdealOfDecidableLE

English

If there is a decidable linear order on ideals, then the ideals form a linear order under inclusion.

Русский

Если существует разрешимый порядок по включению для идеалов, то множество идеалов упорядовано линейно по включению.

LaTeX

$$$ [\\DecidableLE (\\mathrm{Ideal} A)] \\Rightarrow \\mathrm{LinearOrder}(\\mathrm{Ideal} A) $$$

Lean4

instance [DecidableLE (Ideal A)] : LinearOrder (Ideal A) :=
  have := decidableEqOfDecidableLE (α := Ideal A)
  have := decidableLTOfDecidableLE (α := Ideal A)
  Lattice.toLinearOrder (Ideal A)

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