[Merged by Bors] - feat(data/*, order/*) supporting lemmas for characterising well-founded complete lattices

[ocfnash]

---

Note that I have included some extra lemmas even though they are not actually needed (or used). Here is the list of such lemmas together with my justification for including them:

• finset.not_nonempty_iff_eq_empty: seems to be a gap set.not_nonempty_iff_eq_empty already exists
• finset.eq_singleton_iff_nonempty_unique_mem: I introduce set.eq_singleton_iff_nonempty_unique_mem here so it seems worth adding the finset version also
• finset.inf_eq_Inf: I introduce finset.sup_eq_Sup so it seems worth adding the inf version also
• rel_hom.map_inf: I introduce rel_hom.map_sup here so it seems worth adding the inf version also
• Inf_eq_top_nonempty_eq_singleton: I introduce Sup_eq_bot_nonempty_eq_singleton so it seems worth adding the inf version also
• set.finite.preimage_embedding: I used this for an earlier proof of the results here and it seemed worth keeping

I think it is reasonable to bundle these extra results with the other work here but I will happily excise these (or move them to a separate PR) if requested.

[awainverse]

Rather than prove 4 implications, I think you can prove the equivalence of these 3 conditions with 3 implications. The most logical way to me, without having written any code, would be well_founded -> is_sup_finite_compact -> is_sup_closed_compact.

I'd also rewrite is_sup_finite_compact to be about finsets, but that's an easy equivalence, so you could still use finset API if you don't do this.

The following are suggestions for how to prove some of those directions. I'll investigate these further if I have time. Feel free not to use them if you don't want to, and I'm sorry if some of this is just rehashing what you've already done.

I'd prove well_founded -> is_sup_finite_compact by considering the set of all sups of finsets in your lattice. That's got to have a maximal element, which you can show is the Sup of the whole set.

There should be a quick proof of is_sup_finite_compact -> is_sup_closed_compact by selecting a finset such that finset.sup t = Sup s, and then show by induction (if it's not already in the library) that a set closed under sup will also be closed under finset.sup.

[eric-wieser]

Golfs to

Suggested change

	by { rw set.eq_singleton_iff_nonempty_unique_mem, rw Inf_eq_top at h_inf, exact ⟨hne, h_inf⟩, }
	set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨hne, Inf_eq_top.mp h_inf⟩

I'm sure you can do something similar with the one below

[ocfnash]

I have mixed feelings about this one. I do use term-mode proofs but whenever I'm on the fence, I avoid them because they're harder to read (and, I claim, maintain).

Still, commit away if you like!

[urkud]

Could you please move supporting lemmas to a separate PR?

[urkud]

Once you have all implications, could you please add

• a tfae lemma?
• 3 convenience lemmas with iffs?
• dot-style lemmas for missing implications (can be done using command alias)?

[ocfnash]

Thanks for the review @urkud I have just one question. When you say:

Could you please move supporting lemmas to a separate PR?

do you mean the six "extra" lemmas I mentioned at the very top of this PR, or do you mean all lemmas, e.g., everything except for the contents of complete_well_founded.lean?

Either way, I'm happy to do it!

[urkud]

I mean all changes to existing files.

[ocfnash]

I mean all changes to existing files.

Done!

[urkud]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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