English
Let P be a semilattice with join, directed by ≥. For any two ideals I and J of P, their meet in the lattice of ideals equals their intersection, i.e., I ∧ J = I ∩ J.
Русский
Пусть P — полупорядоченное множество с операцией объединения ⊔ и направленностью по отношению ≥. Тогда для любых идеалов I и J множества P их инфимум в решетке идеалов равен их пересечению: I ∧ J = I ∩ J.
LaTeX
$$$ \forall I,J \in \mathrm{Ideal}(P),\ I \wedge J = I \cap J.$$$
Lean4
/-- The infimum of two ideals of a co-directed order is their intersection. -/
instance : Min (Ideal P) :=
⟨fun I J ↦
{ toLowerSet := I.toLowerSet ⊓ J.toLowerSet
nonempty' := inter_nonempty I J
directed' := fun x hx y hy ↦ ⟨x ⊔ y, ⟨sup_mem hx.1 hy.1, sup_mem hx.2 hy.2⟩, by simp⟩ }⟩
