English
The family of ideals forms an InfSet; the infimum of any set S of ideals is an ideal.
Русский
Семейство идеалов образует InfSet; инфимум любой множества S идеалов является идеалом.
LaTeX
$$$ \text{InfSet}(\mathrm{Ideal}(P)) ext{ exists and yields the greatest lower bound of } S. $$$
Lean4
instance : InfSet (Ideal P) :=
⟨fun S ↦
{ toLowerSet := ⨅ s ∈ S, toLowerSet s
nonempty' :=
⟨⊥, by
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]
exact fun s _ ↦ s.bot_mem⟩
directed' := fun a ha b hb ↦
⟨a ⊔ b,
⟨by
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂] at ha hb ⊢
exact fun s hs ↦ sup_mem (ha _ hs) (hb _ hs), le_sup_left, le_sup_right⟩⟩ }⟩
