Sup in nat belongs to set

Stream: Is there code for X?

[Vladimir Goryachev]

Hello everyone. I have a subset of natural numbers, for which I can prove it is bounded and nonempty. How do I show that its Sup belongs to it? (And also, should I use Sup there or something else?)

[Vladimir Goryachev]

Or maybe I should ask, how do I best write "the largest n such that this property holds"?

[Ruben Van de Velde]

Your approach sounds correct, but I'm finding it surprisingly hard to prove

[Patrick Massot]

Finite stuff in mathlib is a mess, we're sorry about it.

[Johan Commelin]

nat.find gives you the smallest nat with some property.

[Johan Commelin]

In your case, you are looking for the smallest n such that for all m > n, m \notin S.

[Floris van Doorn]

There is docs#nat.has_Sup and docs#nat.Sup_def. It might be missing that the Sup is an element of the set.

[Eric Wieser]

Does docs#finset.max combined with docs#finset.max_eq_sup_with_bot and docs#finset.sup_eq_supr help?

[Vladimir Goryachev]

using rw nat.Sup_def at works, but gives me a nat.find ?m_1. I used to deal with such strings by using erw nat.find_eq_iff at, but this time it does not work. So actually, how does one convert nat.find ?m_1 to something useful?

[Vladimir Goryachev]

I could try to rewrite this using finsets, thank you.

[Ruben Van de Velde]

I managed to do it without finsets in two steps:

import order.conditionally_complete_lattice
lemma sup_in (s : set nat) (h : ∃ n, ∀ a ∈ s, a ≤ n) (h' : set.nonempty s) :
  ∃ m, m ∈ s ∧ ∀ a ∈ s, a ≤ m := sorry
lemma sup_in' (x : set nat) (h : ∃ n, ∀ a ∈ x, a ≤ n) (h' : set.nonempty x) : Sup x ∈ x := sorry

open_locale classical

lemma sup_in (s : set nat) (h : ∃ n, ∀ a ∈ s, a ≤ n) (h' : set.nonempty s) :
  ∃ m, m ∈ s ∧ ∀ a ∈ s, a ≤ m :=
begin
  obtain ⟨n, h⟩ := h,
  induction n with n ih generalizing s,
  { obtain ⟨y, hy⟩ := h',
    have := h y hy,
    simp at this,
    subst this,
    use [0, hy, h] },
  { by_cases hn : n.succ ∈ s,
    {use [n.succ, hn, h]},
    { refine ih s h' _,
      intros a ha,
      have := h a ha,
      rw ←nat.lt_succ_iff,
      apply lt_of_le_of_ne this,
      exact ne_of_mem_of_not_mem ha hn } }
end

lemma sup_in' (x : set nat) (h : ∃ n, ∀ a ∈ x, a ≤ n) (h' : set.nonempty x) : Sup x ∈ x :=
begin
  obtain ⟨m, mmem, mbd⟩ := sup_in x h h',
  convert mmem,
  rw nat.Sup_def h,
  apply le_antisymm,
  { by_contra H,
    rw [not_le] at H,
    exact nat.find_min h H mbd },
  { exact nat.find_spec h _ mmem },
end

[Ruben Van de Velde]

Now I'm waiting for one of the experts to solve it in two lines :)

[Floris van Doorn]

not quite two lines, but a little shorter:

import order.conditionally_complete_lattice

open_locale classical
namespace nat

lemma Sup_mem {s : set ℕ} (h1 : s.nonempty) (h2 : ∃ n, ∀ a ∈ s, a ≤ n) : Sup s ∈ s :=
begin
  rw [Sup_def h2],
  rcases h1 with ⟨n, hn⟩,
  cases h : nat.find h2 with m,
  { convert hn, rw [eq_comm, ← nonpos_iff_eq_zero], convert nat.find_spec h2 n hn, rw h },
  { by_contra h',
    apply nat.find_min h2 ((nat.lt_succ_self m).trans_le h.ge),
    intros k hk,
    rw [← lt_succ_iff], rw [← h] at *,
    exact lt_of_le_of_ne (nat.find_spec h2 k hk) (mt (by { rintro rfl, exact hk }) h') }
end

end nat

[Patrick Massot]

I think all those proofs are not in the relevant generality. I propose:

import order.conditionally_complete_lattice

open set

lemma set.nonempty.Sup_mem {α : Type*} [conditionally_complete_linear_order α] {s : set α}
  (h : s.nonempty) (hs : finite s) : Sup (s : set α) ∈ s :=
begin
  classical,
  revert h,
  apply finite.induction_on hs,
  { simp },
  rintros a t hat t_fin ih -,
  rcases t.eq_empty_or_nonempty with rfl | ht,
  { simp },
  { rw cSup_insert t_fin.bdd_above ht,
    by_cases ha : a ≤ Sup t,
    { simp [sup_eq_right.mpr ha, ih ht] },
    { simp only [sup_eq_left, mem_insert_iff, (not_le.mp ha).le, true_or] } }
end

example {s : set ℕ} (h1 : s.nonempty) (h2 : bdd_above s) : Sup s ∈ s :=
begin
  apply h1.Sup_mem,
  sorry
end

[Patrick Massot]

The sorry asks to prove that a set of natural numbers which is bounded above is finite. I don't know whether we already know that, but we certainly want to prove it anyway

[Patrick Massot]

see #7682

[Eric Wieser]

Is the statement also true for complete linear orders, without the finiteness assumptions?

[Alistair Tucker]

(deleted)

[Kevin Buzzard]

Sup of open interval (0,1) considered as a subset of complete lattice closed interval [0,1] isn't in the set

[Mario Carneiro]

It is true for (conditionally) complete discrete linear orders without finiteness, I think

[Mario Carneiro]

what you need here is that bounded sets are compact

[Kevin Buzzard]

What's an example of a complete discrete linear order that isn't itself finite?