Is Finset directed?

Stream: maths

[Christopher Hoskin]

This is going a bit outside my mathematical knowledge...

The following is easily proved:

lemma test [DecidableEq α] {s t : Finset α} : ∃ r, s ≤ r ∧ t ≤ r := by
  use (s ⊔ t)
  constructor
  · exact le_sup_left
  . exact le_sup_right

I'm wondering if the statement is still true with the [DecidableEq α] hypothesis removed? Intuitively it feels like it ought to be?

Christopher

[Yury G. Kudryashov]

Do you want a proof that doesn't use Classical.choice? If no, then you can use by classical; apply directed_of_sup

[Yury G. Kudryashov]

See also docs#SemilatticeSup.to_isDirected_le

[Yury G. Kudryashov]

I think that we should add an instance

instance : IsDirected (Finset α) (· ≤ ·) := by classical infer_nstance

if we don't have it yet.

[Yury G. Kudryashov]

Also, many lemmas (e.g., about docs#Filter.atTop) can be generalized from SemilatticeSup to IsDirected. They were written for semilattices because IsDirected wasn't there back then.

[Christopher Hoskin]

So,

instance [SemilatticeSup α] : IsDirected  (Finset α) (· ⊆ ·) :=
  show IsDirected (Finset α) (· ≤ ·) by classical infer_instance

?

[Kevin Buzzard]

No, you don't want to assume alpha is a SemilatticeSup

[Yury G. Kudryashov]

Linter will catch this.

[Yury G. Kudryashov]

@Christopher Hoskin We should have instances both for (· ≤ ·) and (· ⊆ ·)

[Christopher Hoskin]

Thanks. I was trying to add it here after importing Mathlib.Order.Directed. The infer instance doesn't seem to work though. If I put it in another file which imports Mathlib.Order.Directed and Mathlib.Data.Finset.Basic then it does work.

[Yury G. Kudryashov]

It should go after the Lattice instance

[Christopher Hoskin]

Okay, so I was now expecting to be able to do:

lemma test (α : Type _) {s t : Finset α} : ∃ r, s ≤ r ∧ t ≤ r := by
  use (directed_of (· ⊆ ·) s t)

But I get failed to synthesize instance IsDirected (Finset α) fun x x_1 ↦ x ⊆ x_1

[Yury G. Kudryashov]

Please post a #mwe

[Christopher Hoskin]

Against the current master branch:

import Mathlib.Data.Finset.Basic
instance : IsDirected  (Finset α) (· ⊆ ·) :=
  show IsDirected (Finset α) (· ≤ ·) by classical infer_instance

lemma test1 {s t : Finset α} : ∃ r, s ≤ r ∧ t ≤ r := by
  use (directed_of (· ⊆ ·) s t)

lemma test2 {s t : Finset α} : ∃ r, s ≤ r ∧ t ≤ r := by
  classical
    use (directed_of (· ⊆ ·) s t)

[Yury G. Kudryashov]

Looks like a bug in use

[Yury G. Kudryashov]

Try exact or just := directed_of _ _ _

[Yury G. Kudryashov]

But you'll need instances both for le and subset.

[Christopher Hoskin]

Thanks very much, that worked.

Now, what if I wanted to prove something like:

lemma test2  (s : Set α) (f₁ f₂ : Finset α) (hf₁ : ↑f₁ ⊆ s) (hf₂ : ↑f₂ ⊆ s) :
    ∃ (f : Finset α), (↑f ⊆ s)∧(f₁ ≤ f)∧(f₂ ≤ f) := sorry

Again, this is easy enough with [DecidableEq α]

lemma test2 [DecidableEq α] (s : Set α) (f₁ f₂ : Finset α) (hf₁ : ↑f₁ ⊆ s) (hf₂ : ↑f₂ ⊆ s) :
    ∃ (f : Finset α), (↑f ⊆ s)∧(f₁ ≤ f)∧(f₂ ≤ f) := by
  use (f₁ ⊔ f₂)
  constructor
  · intros c hc
    simp at hc
    cases' hc with h₁ h₂
    exact hf₁ h₁
    exact hf₂ h₂
  · constructor
    · exact le_sup_left
    · exact le_sup_right

My guess is one uses the fact that there's a (g : Finset α) such that (f₁ ≤ g)∧(f₂ ≤ g) and then somehow construct (f : Finset α) to be the elements x of g which have the property x∈s?

[Yaël Dillies]

At this point I would just suggest using classical and taking f = f₁ ∪ f₂.

[Christopher Hoskin]

Thanks, that works! (My other idea was to work over Finset { a : α // a ∈ s} instead of Finset α).