## Stream: new members

### Topic: Complete lattices and subsets

#### Ryan Lahfa (Mar 22 2020 at 21:51):

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 (Mar 22 2020 at 21:52):

There are things like semilattice_inf if this helps.

#### Kevin Buzzard (Mar 22 2020 at 21:52):

There are a gazillion kinds of lattice.

#### Ryan Lahfa (Mar 22 2020 at 21:52):

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 (Mar 22 2020 at 21:53):

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

#### Ryan Lahfa (Mar 22 2020 at 21:54):

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 (Mar 22 2020 at 21:54):

I just made up semilattice_inf, hang on.

#### Kevin Buzzard (Mar 22 2020 at 21:55):

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

#### Kevin Buzzard (Mar 22 2020 at 21:56):

There is a ton of stuff in order.lattice

#### Ryan Lahfa (Mar 22 2020 at 21:57):

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 (Mar 22 2020 at 21:58):

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 (Mar 22 2020 at 21:59):

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

#### Kevin Buzzard (Mar 22 2020 at 22:16):

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

#### Kevin Buzzard (Mar 22 2020 at 22:16):

It certainly exists.

#### Kevin Buzzard (Mar 22 2020 at 22:18):

infi is in order.complete_lattice

#### Kevin Buzzard (Mar 22 2020 at 22:18):

as is Inf

#### Kevin Buzzard (Mar 22 2020 at 22:19):

I see, there is nothing about them

#### Ryan Lahfa (Mar 22 2020 at 22:20):

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 (Mar 22 2020 at 22:21):

You can just make what you want, right?

#### Ryan Lahfa (Mar 22 2020 at 22:21):

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 (Mar 22 2020 at 22:21):

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 (Mar 22 2020 at 22:24):

Yeah you should talk to a more latticy person.

#### Mario Carneiro (Mar 23 2020 at 02:38):

Existence of Inf implies existence of Sup and vice versa

#### Mario Carneiro (Mar 23 2020 at 02:39):

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

@Ryan Lahfa

#### Yury G. Kudryashov (Mar 23 2020 at 02:42):

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 (Mar 23 2020 at 02:56):

I thought that already existed

#### Yury G. Kudryashov (Mar 23 2020 at 02:58):

Can't find it in complete_lattice.

#### Ryan Lahfa (Mar 23 2020 at 10:54):

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 (Mar 23 2020 at 10:55):

Make it a simp-lemma if the instance exists.

#### Johan Commelin (Mar 23 2020 at 10:55):

Then it doesn't vanish completely

#### Johan Commelin (Mar 23 2020 at 10:56):

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

#### Ryan Lahfa (Mar 23 2020 at 10:57):

Sounds good!

Last updated: Dec 20 2023 at 11:08 UTC