Complete lattices and subsets

Stream: new members

[Ryan Lahfa]

Continuing on my example of defining a sequence of strictly increasing elements based on some hypothesis over orders.

I'm trying to see what are the minimal hypothesis on the order to define such a sequence. Mathematically, it seems like I only need to have the existence of min over the set S of X.

lemma st_increasing_seq [linear_order X] {S: set X} (Hlattice: complete_lattice S) (Hinf: set.infinite S):
  (∀ M ⊆ S, M.nonempty → (complete_lattice.Inf M ∈ M)) → ∃ x : ℕ → X, st_increasing x ∧ (range x) ⊆ S := sorry

The closest to I wanted was complete_lattice (but it also requires sups…), I wanted to use semilattice for infs only but it does not define a Inf over sets.

Worse, the above code does not type-check because it complains about the fact that X is not a complete lattice, which I understand.
But at the same time, I don't want all X to be a complete lattice, it could be a conditionally complete lattice in fact only.

Also, it seems like what I really want is (S, ≤) is well-ordered, maybe it could solve everything.

What's the best thing to do?

[Kevin Buzzard]

There are things like semilattice_inf if this helps.

[Kevin Buzzard]

There are a gazillion kinds of lattice.

[Ryan Lahfa]

It does not declare a Inf: set a → a, right? https://leanprover-community.github.io/mathlib_docs/order/lattice.html#lattice.to_semilattice_inf

[Kevin Buzzard]

There's a difference between inf (inf of two elements) and Inf (inf of arbitrary set of elements)

[Ryan Lahfa]

Indeed, so that's why I resorted to complete_lattice / conditionally_complete_lattice which seems to be the only one to declare the Inf (and not inf).

[Kevin Buzzard]

I just made up semilattice_inf, hang on.

[Kevin Buzzard]

Can you ask your question again? I don't really know what I'm looking for.

[Kevin Buzzard]

There is a ton of stuff in order.lattice

[Ryan Lahfa]

I would like to be able to take the Inf of a set, without supposing that there is a complete_lattice over X (the type), but over the set S and be able to get the complete_lattice property for all subsets of S.

[Ryan Lahfa]

let's say X = R, S = [a, +infty[, if you prefer. S is a semilattice_inf and all its subsets too.
But right now, I don't know how to translate those facts in Lean.

[Ryan Lahfa]

I don't see any Inf in order.lattice, it does not define operations over arbitrary sets. :/

[Kevin Buzzard]

I really don't know my way around the lattice stuff. Is it called infi?

[Kevin Buzzard]

It certainly exists.

[Kevin Buzzard]

infi is in order.complete_lattice

[Kevin Buzzard]

as is Inf

[Kevin Buzzard]

I see, there is nothing about them

[Ryan Lahfa]

Kevin Buzzard said:

I really don't know my way around the lattice stuff. Is it called infi?

As far as I understand it, infi is indexed inf, which is something I don't think I need

[Kevin Buzzard]

You can just make what you want, right?

[Ryan Lahfa]

Kevin Buzzard said:

I see, there is nothing about them

I could PR something to add Inf for semilattice_inf, etc, if that's something mathlib would be interested in. But I'd need some guidance for math relevance.

[Ryan Lahfa]

Kevin Buzzard said:

You can just make what you want, right?

Indeed, just wanted to ensure that I was not reinventing the wheel.

[Kevin Buzzard]

Yeah you should talk to a more latticy person.

[Mario Carneiro]

Existence of Inf implies existence of Sup and vice versa

[Mario Carneiro]

Actually, I think you want to not have any lattice like assumption, and just have a hypothesis that says every set in M has a minimal element, this exists as a predicate

[Mario Carneiro]

@Ryan Lahfa

[Yury G. Kudryashov]

BTW, probably we should add a constructor for complete_lattice that takes Inf and autogenerates Sup, and use it for submonoids, subgroups etc.

[Mario Carneiro]

I thought that already existed

[Yury G. Kudryashov]

Can't find it in complete_lattice.

[Ryan Lahfa]

Mario Carneiro said:

Actually, I think you want to not have any lattice like assumption, and just have a hypothesis that says every set in M has a minimal element, this exists as a predicate

Looks the simplest way, but I'd need some way to get it for free for obvious fields which verifies complete_linear_order or even conditionnally_complete_linear_order X which are complete_linear_order over a bounded subset.

[Johan Commelin]

Make it a simp-lemma if the instance exists.

[Johan Commelin]

Then it doesn't vanish completely

[Johan Commelin]

Or alternatively provide a special case of the lemma if the instance is there

[Ryan Lahfa]

Sounds good!