Intersection of a chain of nonempty finsets is nonempty.

Stream: Is there code for X?

[Rémi Bottinelli]

Hey, I'm in need of such a function. What would be the shortest way to get it? Thanks!

[Kyle Miller]

Here's one formulation of it:

import data.fintype.basic
import order.chain
import data.nat.lattice

lemma finset.nonempty_Inter_of_chain {α : Type*}
  (sf : set (finset α)) (sfn : sf.nonempty)
  (hn : ∀ s ∈ sf, finset.nonempty s) (hc : is_chain (⊆) sf) :
  ∃ x, ∀ s ∈ sf, x ∈ s :=
begin
  have csn : (finset.card '' sf).nonempty,
  { obtain ⟨s, hs⟩ := sfn,
    use [s.card, s, hs], },
  obtain ⟨s, hs, hsc⟩ := nat.Inf_mem csn,
  obtain ⟨x, hx⟩ := hn _ hs,
  use x,
  intros s' hs',
  have : s.card ≤ s'.card,
  { rw hsc,
    apply nat.Inf_le,
    use [s', hs'], },
  have : s ⊆ s',
  { obtain (rfl|h) := eq_or_ne s s',
    { refl },
    { apply or_iff_not_imp_right.mp (hc hs hs' h),
      intro h',
      cases finset.eq_of_subset_of_card_le h' this,
      exact h rfl } },
  exact this hx,
end

[Rémi Bottinelli]

ah, thanks! You haven't used any \Inter because it doesn't exist yet forfinset, right?

[Kyle Miller]

I just thought (⋂ (s ∈ sf), (s : set α)).nonempty wouldn't help with the proof. No deep reasons.

[Kyle Miller]

It's not too different also showing it for directed sets:

lemma finset.nonempty_Inter_of_chain {α : Type*}
  (sf : set (finset α)) (sfn : sf.nonempty)
  (hn : ∀ s ∈ sf, finset.nonempty s) (hd : directed_on (⊇) sf) :
  ∃ x, ∀ s ∈ sf, x ∈ s :=
begin
  have csn : (finset.card '' sf).nonempty,
  { obtain ⟨s, hs⟩ := sfn,
    use [s.card, s, hs], },
  obtain ⟨s, hs, hsc⟩ := nat.Inf_mem csn,
  obtain ⟨x, hx⟩ := hn _ hs,
  use x,
  intros s' hs',
  have : s ⊆ s',
  { obtain ⟨s'', hs'', h1, h2⟩ := hd _ hs _ hs',
    apply finset.subset.trans _ h2,
    have : s.card ≤ s''.card,
    { rw hsc,
      apply nat.Inf_le,
      use [s'', hs''], },
    cases finset.eq_of_subset_of_card_le h1 this,
    refl, },
  exact this hx,
end

[Yaël Dillies]

Rémi Bottinelli said:

ah, thanks! You haven't used any ⋂ because it doesn't exist yet forfinset`, right?

It does: docs#finset.inf. finset.bUnion is a (stupid according to me) special case of finset.sup.