instPartialOrderIdeal — Mathlib

English

The partial order on Ideals is induced by subset inclusion via SetLike.coe.

Русский

Частичный порядок на Ideals задаётся включением подмножеств через SetLike.coe.

LaTeX

$$$ \\text{PartialOrder}(\\text{Ideal}(P)) \\;\\text{is given by}\\; I \\le J \\iff I.\\text{carrier} \\subseteq J.\\text{carrier} $$$

Lean4

/-- The partial ordering by subset inclusion, inherited from `Set P`. -/
instance instPartialOrderIdeal : PartialOrder (Ideal P) :=
  PartialOrder.lift SetLike.coe SetLike.coe_injective

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