inf of finite non empty directed set

Stream: Is there code for X?

[Patrick Massot]

I cannot find

import Mathlib

open Function Filter Set

example {X : Type*} [CompleteLattice X] {s : Set X} (h : DirectedOn (· ≥ ·) s) (h' : s.Finite)
    (h'' : s ≠ ∅) : sInf s ∈ s := by
  sorry

Did I mess up the statement? @Yaël Dillies

[Yaël Dillies]

Looks true. Will tell you later

[Antoine Chambert-Loir]

I couldn't find it a few weeks ago. I proved some version of it in one of my recent PRs related to the combinatorial Nullstellensatz...

[Antoine Chambert-Loir]

https://github.com/leanprover-community/mathlib4/blob/bb46d419c7392ff100fa428e9ba492c10190c036/Mathlib/Data/Finset/Lattice.lean#L634

[Patrick Massot]

Thanks Antoine, but your version assumes the order relation is total so it’s a lot less tricky.

[Patrick Massot]

Earlier today I quickly tried to use Finset.induction_on but very soon I decided Yaël probably knew how to find or prove this lemma way more efficiently.

[Jireh Loreaux]

I think we don't have it currently, because we do have docs#Set.Nonempty.csInf_mem, which unncessarily assumes the order in linear. I assume because the proof ultimately uses docs#Finset.Nonempty.csInf_eq_min', which does need that assumption.

[Jireh Loreaux]

(sorry, to be clear: unnecessary if the set is directed)

[Bhavik Mehta]

import Mathlib

/--
If a transitive `r` is directed on `{a} ∪ s`, and `a` is not the `r`-maximum of `s`, then `r` is
directed on `s`.
Note the maximality assumption is necessary, as if the `r`-maximum of `s` (exists and) is `a`, then
`r` is trivially directed on `{a} ∪ s`, and we cannot deduce anything about how it behaves on `s`.
(A concrete counterexample to the statement without `h'` is given by `r x a` for every `x ∈ s`, and
no other relations.)
-/
lemma DirectedOn.of_insert {X : Type*} {r : X → X → Prop} (hr : Transitive r)
    {s : Set X} {a : X} (h : DirectedOn r (insert a s)) (h' : ∃ x ∈ s, ¬ r x a) :
    DirectedOn r s := by
  intro p hp q hq
  obtain ⟨x, hx, hx'⟩ := h'
  obtain ⟨b, hb₁, hb₂, hb₃⟩ := h p (.inr hp) x (.inr hx)
  obtain ⟨c, hc₁, hc₂, hc₃⟩ := h b hb₁ q (.inr hq)
  have : c ≠ a := by
    rintro rfl
    exact hx' (hr hb₃ hc₂)
  exact ⟨c, hc₁.resolve_left this, hr hb₂ hc₂, hc₃⟩

lemma Finset.sup'_mem_of_le_directedOn {X : Type*} [SemilatticeSup X] {s : Finset X}
    (h : DirectedOn (· ≤ ·) s.toSet) (h' : s.Nonempty) : s.sup' h' id ∈ s := by
  induction s using Finset.cons_induction_on
  case h₁ => simp at h'
  case h₂ a s has ih =>
    obtain rfl | hs := s.eq_empty_or_nonempty
    case inl => simp
    simp only [id_eq, hs, sup'_cons, mem_cons, sup_eq_left, sup'_le_iff, or_iff_not_imp_left,
      not_forall, exists_prop, forall_exists_index, and_imp]
    intro x hx hax
    have h₁ : DirectedOn (· ≤ ·) s.toSet := .of_insert transitive_le (by simpa using h) ⟨x, hx, hax⟩
    obtain ⟨y, hy, hy', hy''⟩ := h a (by simp) (s.sup' hs (·)) (mem_cons_of_mem (ih h₁ hs))
    have hya : y ≠ a := (False.elim <| hax <| · ▸ (le_sup' id hx).trans hy'')
    have hys : y ∈ s := (mem_cons.1 hy).resolve_left hya
    have : s.sup' hs (·) = y := hy''.antisymm (le_sup' id hys)
    rwa [this, sup_of_le_right hy']

lemma Finset.inf'_mem_of_ge_directedOn {X : Type*} [SemilatticeInf X] {s : Finset X}
    (h : DirectedOn (· ≥ ·) s.toSet) (h' : s.Nonempty) : s.inf' h' id ∈ s :=
  @Finset.sup'_mem_of_le_directedOn Xᵒᵈ _ _ h h'

lemma Finset.sInf_mem_of_ge_directedOn {X : Type*} [CompleteLattice X] {s : Finset X}
    (h : DirectedOn (· ≥ ·) s.toSet) (h' : s.Nonempty) : sInf s ∈ s := by
  rw [← inf_id_eq_sInf, ← inf'_eq_inf h']
  exact Finset.inf'_mem_of_ge_directedOn h _

lemma Set.Finite.sInf_mem_of_ge_directedOn {X : Type*} [CompleteLattice X] {s : Set X}
    (h : DirectedOn (· ≥ ·) s) (h' : s.Finite)
    (h'' : s.Nonempty) : sInf s ∈ s := by
  have hs' : h'.toFinset.Nonempty := by simpa
  simpa using Finset.sInf_mem_of_ge_directedOn (by simpa) hs'

[Patrick Massot]

Thanks @Bhavik Mehta Do you plan to PR this to Mathlib?

[Bhavik Mehta]

I think all the above lemmas should be in mathlib - I'll make a PR on Monday unless someone beats me to it, I don't mind who makes it!

[Antoine Chambert-Loir]

Will that general version immediately imply mine (where I assume the ordering relation is total)? Because it seemed to be missing as well.

[Yaël Dillies]

Yes, it will, although we seem to be missing the lemma saying that a set in a linear order is directed

[Antoine Chambert-Loir]

Hence for the moment it won't!

[Bhavik Mehta]

The version for a complete linear order order is much easier:

lemma Finset.sInf_mem {X : Type*} [CompleteLinearOrder X] {s : Finset X}
    (h' : s.Nonempty) : sInf s ∈ s := by
  rw [h'.csInf_eq_min']
  exact Finset.min'_mem _ _

lemma Set.Finite.sInf_mem {X : Type*} [CompleteLinearOrder X] {s : Set X}
    (h' : s.Finite) (h'' : s.Nonempty) : sInf s ∈ s := by
  have hs' : h'.toFinset.Nonempty := by simpa
  simpa using Finset.sInf_mem_of_ge hs'