Max element of a set

Stream: new members

[Joe]

I want to define something like this:

def M (N : ℕ) (x : α) : ℕ := max {m ≤ N | x ∈ s m}

I don't know how to say this in Lean. I end up using finset, but it looks really complicated. I don't know if it is the right way.

import data.finset
noncomputable theory
local attribute [instance] classical.prop_decidable

section
variables {α : Type*} (s : ℕ  → set α)

def M (N : ℕ) (x : α) : ℕ :=
  finset.max'
    (finset.filter (λ m, x ∈ s m) (finset.range (N+1)))
      (sorry) -- the set above is nonempty

end

[Kevin Buzzard]

What do you want the answer to be if no such m exists? I mean -- if the set is empty?

[Joe]

I can somehow guarantee it is not empty.

[Joe]

But I think let it be 0 will be fine too, because it will not happen anyways.

[Joe]

I find this in Isabelle, another theorem prover

define m where [abs_def]: "m N x = Max {m. m ≤ N ∧ x ∈ (⋃n≤N. B m n)}" for N x

So I think if I can do this in lean that will be good

[Joe]

Said in another way,
if
x ∈ ⋃ (M ≤ N), ⋃ (k ≤ N), A M k
then
find the largest M such that x ∈ ⋃ (k ≤ N), A M k
and then
find the largest k such that x ∈ A M k

[Kevin Buzzard]

The finset approach looks fine to me. One way to fill in the sorry would be if h : (the hypothesis you need) then finset.max' ... h else 37

[Mario Carneiro]

@Joe In the particular case of the isabelle definition, that max is ranging over natural numbers, and there is a function specifically for that in lean: nat.find_greatest P n is Max {m <= n | P m}

[Kevin Buzzard]

Aah, I'd forgotten about that. I remembered nat.find but I think that one finds the smallest one :-)