Defining element, given its existence and uniqueness

Stream: new members

[Lucas Polymeris]

I'm working with finite lattices, and I would like to give a special name to the bottom element which I've proven exists:

variables {α : Type u} [fin: fintype α] [lat: lattice α] [nempty : nonempty α]
include fin lat nempty

lemma exists_bot : ∃! x : α, ∀ y : α, x ≤ y := by sorry,

How could I do this?

[Yakov Pechersky]

That element is already called bot, and is written \bot

[Yakov Pechersky]

(deleted)

[Lucas Polymeris]

No it is not, just of bunded_lattices

[Yakov Pechersky]

You're right.

[Yakov Pechersky]

You can use fintype.choose

[Yakov Pechersky]

docs#fintype.choose

[Lucas Polymeris]

thanks. Do you know if I can prove a structure to _be_ other? Like if I could prove that $\alpha$ is also a bounded_lattice would also be nice

[Alex J. Best]

To make your example a #mwe please include the imports and variables so we don't have to guess them e.g:

import data.finset.lattice
import data.fintype.basic
universe u
variables {α : Type u} [fin: fintype α] [lat: lattice α] [nempty : nonempty α]
include fin lat nempty

lemma exists_bot : ∃! x : α, ∀ y : α, x ≤ y := by sorry

[Alex J. Best]

For the second question you can do:

lemma exists_bot : ∃! x : α, ∀ y : α, x ≤ y := by sorry
instance : bounded_lattice α :=
{ top := _,
  bot := _,
  le_top := _,
  bot_le := _,
  ..(show lattice α, by apply_instance) }

[Lucas Polymeris]

Sorry, mb, I'm working with the following setup

import order.basic order.lattice data.fintype.basic data.finset.basic algebra.order

universe u

section mysec
variables {α : Type u} [fin: fintype α] [lat: lattice α] [nempty : nonempty α]
include fin lat nempty

def minimum (x : α) := ∀ y : α, x ≤ y

lemma exists_bot : ∃! x : α, minimum x := by sorry

[Yakov Pechersky]

I'd do this via docs#fin.bounded_lattice and the fin to fintype order iso whose name I can never recall

[Lucas Polymeris]

Alex J. Best said:

For the second question you can do:

lemma exists_bot : ∃! x : α, ∀ y : α, x ≤ y := by sorry
instance : bounded_lattice α :=
{ top := _,
  bot := _,
  le_top := _,
  bot_le := _,
  ..(show lattice α, by apply_instance) }

it_complaints that a declaration named bounded_lattice has already been declared. Does this mean is already in some of my imports the fact that a finite lattice is bounded?

[Yakov Pechersky]

No, it just means that the autogenerated name clashes with an existing name, afaiu.

[Alex J. Best]

You can do it like this I guess:

lemma exists_bot : ∃! x : α, ∀ y : α, x ≤ y := by sorry
instance fintype.bounded_lattice : bounded_lattice α :=
{ bot := classical.some exists_bot.exists,
  top := order_dual.of_dual $ classical.some exists_bot.exists,
  le_top := begin
    intro a,
    rw ← order_dual.le_to_dual,
    exact (classical.some_spec exists_bot.exists) _,
  end,
  bot_le := classical.some_spec exists_bot.exists ,
  ..(show lattice α, by apply_instance) }

[Alex J. Best]

It's probably easier to read to just prove existence of the bot element, then you'll get uniqueness from that

[Alex J. Best]

Exists unique isn't really used so much in mathlib, you're just packing up two facts into one.

[Eric Wieser]

Is #7123 relevant here?

[Eric Wieser]

Specifically the fintype.bounded_lattice it provides

[Alex J. Best]

It even does everything constructively :smile:

[Yakov Pechersky]

Does it have the following?

@[reducible] def lattice.of_order_iso [lattice α] (f : α ≃o β) : lattice β :=
{ sup := λ b b', f (f.symm b ⊔ f.symm b'),
  le := (≤),
  le_refl := λ b, f.symm.le_iff_le.mp (le_refl _),
  ...-- sorry
  }

@[reducible] def bounded_lattice.of_order_iso [bounded_lattice α] (f : α ≃o β) :
bounded_lattice β :=
{ top := f ⊤,
  bot := f ⊥,
  le_top := λ _, f.symm_apply_le.mp le_top,
  bot_le := λ b, f.le_symm_apply.mp bot_le,
  ..lattice.of_order_iso f }

[Yakov Pechersky]

Ah I guess I need linear_order α to use docs#finset.order_iso_of_fin

[Yakov Pechersky]

btw fintype.choose is also constructive. fintype.choose or finset.fold might have different performance characteristics -- the latter will terminate on finding the bot element, but verifying that it is the bot element requires checking <= for all elements. So worst-case is N^2.

[Lucas Polymeris]

I was trying to prove Birkhoff's representation theorem for distributive lattices. And indeed Idid, but I ended up using
bounded_distrib_lattice as the base type. Later I would still like to prove it from fintype and lattice. But for now this is what I'v got. If anyone wants to criticize the work ,I'll be happy to learn from your comments, and thank's for the ones already made. I'll now try to figure out that part.