Pi of directed sets

Stream: maths

[Christopher Hoskin]

I'm trying to show that the Pi of directed sets is directed:

variable {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)]

lemma prodMk {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (· ≤ ·) (d i)) :
    DirectedOn (· ≤ ·) (Set.pi  Set.univ d) := by
  intro a ha b hb
  let h := fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
  obtain ⟨c, hc⟩ : ∃ (c : (i : ι) → α i), ∀ (i : ι), a i ≤ c i ∧ b i ≤ c i := sorry

I'm not sure how to go about obtaining c fromh though?

Christopher

[Eric Wieser]

Does choose f hf using h work?

[Eric Wieser]

lemma prodMk {d : (i : ι) → Set (α i)} (hd : ∀ (i : ι), DirectedOn (· ≤ ·) (d i)) :
    DirectedOn (· ≤ ·) (Set.pi  Set.univ d) := by
  intro a ha b hb
  dsimp
  let h := fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
  choose f hf using h
  simpa [Pi.le_def, ← forall_and] using ⟨f, hf⟩

[Christopher Hoskin]

Eric Wieser said:

Does choose f hf using h work?

Yes, that works! Thank you.

Christopher