construct expression from infinite set

Stream: new members

[Shi Zhengyu]

like if I wish the max of the set to be stored in k, along with a lemma that says forall i:N, i \in S -> i <= k.

[Alex J. Best]

The max of an infinite set may not exist in general though. What is the type that you have a set of to begin with (e.g. natural numbers? some type with an order).

[Shi Zhengyu]

That's true. I am working with a set of upper-bounded natural numbers.

[Alex J. Best]

Ok you should be able to express what you want using the following

import order.conditionally_complete_lattice
import tactic
import data.nat.lattice

lemma test (a : set ℕ) (h : bdd_above a) : false :=
begin
  let k := Sup a,
  have h_le_k : ∀ (x : ℕ) (hx : x ∈ a), x ≤ k := λ x hx, le_cSup h hx,
end

[Alex J. Best]

This shows roughly how to set up a lemma about a bounded above set of naturals and take the max, and the defining property of the max.