toIdeal — Mathlib

English

If x ≤ y and x ∉ I, then y ∉ I for I an ideal in P.

Русский

Если x ≤ y и x не принадлежит I, то y не принадлежит I, где I — идеал в P.

LaTeX

$$$ x \\le y \\Rightarrow x \\notin I \\Rightarrow y \\notin I $$$

Lean4

/-- Create an element of type `Order.Ideal` from a set satisfying the predicate
`Order.IsIdeal`. -/
def toIdeal [LE P] {I : Set P} (h : IsIdeal I) : Ideal P :=
  ⟨⟨I, h.IsLowerSet⟩, h.Nonempty, h.Directed⟩

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