# Zulip Chat Archive

## 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

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

@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 `submonoid`

s, `subgroup`

s 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: May 08 2021 at 09:11 UTC