English
The ideals of P form a lattice under inclusion, with meet given by intersection and join given by the rule above: I ∧ J = I ∩ J and I ∨ J = { x ∈ P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j }.
Русский
Идеалы P образуют решетку по включению: встреча равна пересечению, объединение задаётся правилом I ∨ J = { x ∈ P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j }.
LaTeX
$$$ \mathrm{Ideal}(P) \text{ является решеткой с } I \wedge J = I \cap J \text{ и } I \lor J = \{ x \in P \mid \exists i \in I, \exists j \in J, x \le i \lor j \}. $$$
Lean4
instance : Lattice (Ideal P) :=
{ Ideal.instPartialOrderIdeal with
sup := (· ⊔ ·)
le_sup_left := fun _ J i hi ↦
let ⟨w, hw⟩ := J.nonempty
⟨i, hi, w, hw, le_sup_left⟩
le_sup_right := fun I _ j hj ↦
let ⟨w, hw⟩ := I.nonempty
⟨w, hw, j, hj, le_sup_right⟩
sup_le := fun _ _ K hIK hJK _ ⟨_, hi, _, hj, ha⟩ ↦
K.lower ha <| sup_mem (mem_of_mem_of_le hi hIK) (mem_of_mem_of_le hj hJK)
inf := (· ⊓ ·)
inf_le_left := fun _ _ ↦ inter_subset_left
inf_le_right := fun _ _ ↦ inter_subset_right
le_inf := fun _ _ _ ↦ subset_inter }
