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


I win

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

I guess Sup and Inf are defined differently now?

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

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.

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 :-)

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