# Zulip Chat Archive

## Stream: general

### Topic: set is a complete lattice

#### Kenny Lau (Apr 13 2018 at 14:57):

mathlib proof:

instance lattice_set : complete_lattice (set α) := { lattice.complete_lattice . le := (⊆), le_refl := subset.refl, le_trans := assume a b c, subset.trans, le_antisymm := assume a b, subset.antisymm, lt := λ x y, x ⊆ y ∧ ¬ y ⊆ x, lt_iff_le_not_le := λ x y, iff.refl _, sup := (∪), le_sup_left := subset_union_left, le_sup_right := subset_union_right, sup_le := assume a b c, union_subset, inf := (∩), inf_le_left := inter_subset_left, inf_le_right := inter_subset_right, le_inf := assume a b c, subset_inter, top := {a | true }, le_top := assume s a h, trivial, bot := ∅, bot_le := assume s a, false.elim, Sup := λs, {a | ∃ t ∈ s, a ∈ t }, le_Sup := assume s t t_in a a_in, ⟨t, ⟨t_in, a_in⟩⟩, Sup_le := assume s t h a ⟨t', ⟨t'_in, a_in⟩⟩, h t' t'_in a_in, Inf := λs, {a | ∀ t ∈ s, a ∈ t }, le_Inf := assume s t h a a_in t' t'_in, h t' t'_in a_in, Inf_le := assume s t t_in a h, h _ t_in }

my proof:

instance lattice_set : complete_lattice (set α) := lattice.complete_lattice_fun

#### Kenny Lau (Apr 13 2018 at 14:57):

I win

#### Gabriel Ebner (Apr 13 2018 at 15:03):

I guess `Sup`

and `Inf`

are defined differently now?

#### Kenny Lau (Apr 13 2018 at 15:04):

really?

#### Gabriel Ebner (Apr 13 2018 at 15:12):

They should be equal. However I don't think they are definitionally equal. `Sup s a = (∃ b ∈ set.image (λ f, f a) s, b) = (∃ b, (∃ c, s c ∧ s c a = b) → b)`

which is different

#### Kenny Lau (Apr 13 2018 at 15:13):

well one could prove that they are equal

#### Kenny Lau (Apr 13 2018 at 15:13):

simp lemma

#### Gabriel Ebner (Apr 13 2018 at 15:15):

This still doesn't give you definitional reduction. If you want to prove `a ∈ Sup s`

, you'll now always need to `simp`

first. There are quite a few places where we accept some additional complexity in order to guarantee good definitional reduction, the `lt`

in preorder is another place. We can define `lt`

in terms of `le`

, but we want it to reduce differently for natural numbers.

#### Kenny Lau (Apr 13 2018 at 15:15):

I see

#### Kevin Buzzard (Apr 13 2018 at 15:29):

Yes, for nat, `a<b`

is _defined_ to be `succ a <= b`

and if you know this you can write some neat obfuscated code :-)

#### Kenny Lau (Apr 13 2018 at 15:29):

such as?

#### Kevin Buzzard (Apr 13 2018 at 15:30):

I believe I used this to do some golf question here a week or two ago. Either a question of Chris or of Nima.

#### Chris Hughes (Apr 13 2018 at 15:37):

It just means that you never have to use the lemma `succ_le_of_lt`

#### Johannes Hölzl (Apr 13 2018 at 15:44):

you can `match`

or use the equation compiler to do case analysis and inductionon `<`

, with the definition following the default setup this would be not possible.

Last updated: May 14 2021 at 03:27 UTC