Directedness and ideals

Stream: general

[Yaël Dillies]

Am I right in thinking that docs#order.ideal.ideal_inter_nonempty is equivalent to is_directed P (swap (≤))?

[Yaël Dillies]

and similarly docs#order.ideal.ideal_Inter_nonempty should be equivalent to a strong directedness which should be satisfied by a complete_latlice.

[Yaël Dillies]

Yup

import order.ideal

open order.ideal

example : ideal_inter_nonempty P ↔ is_directed P (swap (≤)) :=
begin
  split,
  { introI,
    exact ⟨λ a b, inter_nonempty (principal a) (principal b)⟩ },
  { introI,
    refine ⟨λ I J, _⟩,
    obtain ⟨a, ha⟩ := I.nonempty,
    obtain ⟨b, hb⟩ := J.nonempty,
    obtain ⟨c, hac, hbc⟩ := directed_of (swap (≤)) a b,
    exact ⟨c, I.mem_of_le hac ha, J.mem_of_le hbc hb⟩ }
end

[Yaël Dillies]

cc @Noam Atar

[Yaël Dillies]

Actually, strong directedness is just the existence of a bottom element (doesn't have to be order_bot).

[Yaël Dillies]

#11421