[Merged by Bors] - feat(order/lattice): "algebraic" constructors for (semi-)lattices

[bryangingechen]

I also added a module doc string for order/lattice.lean.

---

[eric-wieser]

I don't know if this is Kosher, but:

Suggested change

	{ inf := (⊓),
	le := λ a b, a = a ⊓ b,
	le_refl := λ a, (inf_idem a).symm,
	le_trans := λ a b c hab hbc,
	begin
	dsimp only [(≤)] at *,
	rw [hab, inf_assoc, ←hbc],
	end,
	le_antisymm := λ a b hab hba,
	begin
	dsimp only [(≤)] at *,
	rw [hba, inf_comm, ←hab],
	end,
	inf_le_left := λ a b, show a ⊓ b = a ⊓ b ⊓ a, by rw [inf_comm, inf_assoc, inf_idem],
	inf_le_right := λ a b, show a ⊓ b = a ⊓ b ⊓ b, by rw [inf_assoc, inf_idem],
	le_inf := λ a b c hac hbc,
	begin
	dsimp only [(≤), preorder.le] at *,
	rwa [←inf_assoc, ←hac],
	end }
	begin
	haveI : semilattice_sup (order_dual α) := semilattice_sup.mk' inf_comm inf_assoc inf_idem,
	haveI i := order_dual.semilattice_inf (order_dual α),
	exact i,
	end

[eric-wieser]

Strictly I think you ought to have a lemma like:

theorem preorder.dual_dual (α : Type*) [H : preorder α] :
  order_dual.preorder (order_dual α) = H :=
preorder.ext $ λ _ _, iff.rfl

but for semilattice_inf, and then use that on the last line.

[bryangingechen]

Not sure what you mean with the last suggestion. It might be easier if you push your changes to this branch?

[bryangingechen]

I made an attempt at incorporating the changes as far as I understood them. I'm not sure what to do with semilattice_inf.dual_dual and semilattice_sup.dual_dual though.

[eric-wieser]

I think those lemmas are worth having whether you use them or not, but maybe @gebner or whoever it was that was worrying about defeq abuse can chime in about how to use them here.

[jcommelin]

Apart from the dual_dual issue, this looks good to me. Lots of docs! Thanks!

Let's Get This Merged

[bryangingechen]

@jcommelin Thanks for taking a look! Do you know how the dual_dual lemmas might be used? I guess I'm not really seeing how @eric-wieser's construction of semilattce_inf.mk' is "defeq abuse". What would the alternative be?

[jcommelin]

Hmm, sorry, I misunderstood what's going on. It's actually fine. Thanks for the PR!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests