## Stream: PR reviews

### Topic: sublattice definition #7093

#### Matúš Behun (Apr 07 2021 at 20:33):

Anybody willing to look at talk about my PR? I am trying to define order/sublattice. I need at least some quick overview if structure is right and what else should I work on to be successful with merge.

#7093

#### Johan Commelin (Apr 07 2021 at 20:39):

@Matúš Behun welcome! (Note that there is a dedicated stream #PR reviews for discussion of specific PRs.)

#### Kevin Buzzard (Apr 07 2021 at 20:39):

Thanks for doing this! PR's have their own stream -- perhaps we should continue this conversation in #PR reviews .

heh :-)

#### Johan Commelin (Apr 07 2021 at 20:40):

First look: this looks pretty good, but there are some style issues.

#### Johan Commelin (Apr 07 2021 at 20:40):

@Matúš Behun please take a look at https://leanprover-community.github.io/contribute/style.html#structuring-definitions-and-theorems

#### Notification Bot (Apr 07 2021 at 21:38):

This topic was moved here from #new members > PR Sublattice by Mario Carneiro

#### Matúš Behun (Apr 07 2021 at 22:02):

@Eric Wieser Thank you for review, I would like to discuss it here and your comment regarding function.injective.lattice

#### Eric Wieser (Apr 07 2021 at 22:06):

I did a big refactor recently that removed a lot of duplication between subobjects, and introduced docs#set_like

#### Eric Wieser (Apr 07 2021 at 22:06):

I would guess you started your branch before that refactor

#### Matúš Behun (Apr 07 2021 at 22:07):

What I wanted to achieve is transformation of sublattice to lattice hence lattice beta. Also any comment regarding how to improve pr by adding theorems or instancing something would be appreciated.

#### Matúš Behun (Apr 07 2021 at 22:08):

Eric Wieser said:

I would guess you started your branch before that refactor

Yes

#### Eric Wieser (Apr 07 2021 at 22:11):

Your function.injective.lattice definition isn't useful because it takes a lattice over L, a function from \b to L, a bunch of proofs about that function... Only to ignore all those things and just produce the same lattice over L it started with!

#### Eric Wieser (Apr 07 2021 at 22:12):

Have a look at src#function.injective.mul_one_class for a very simple example of how that definition should actually look

#### Eric Wieser (Apr 07 2021 at 22:14):

Regarding set_like, you'll want to git fetch origin && git merge origin/master before you try to use it

#### Matúš Behun (Apr 07 2021 at 22:19):

okay thanks for the help

#### Matúš Behun (Apr 13 2021 at 22:05):

function.injective.sublattice - thanks for the example i changed it accordingly, of course i forgot to produce sublattice instead of lattice, still might ask around here how to finish this definition

#### Matúš Behun (Apr 13 2021 at 22:07):

regarding set_coe_sort I've changed all definitions to match new style

#### Eric Wieser (Apr 13 2021 at 22:25):

No, the result really should be lattice, just on the type at the other end of the injective function

#### Eric Wieser (Apr 13 2021 at 22:26):

Perhaps we already have that definition as docs#lattice.lift (to match docs#partial_order.lift)?

Last updated: May 09 2021 at 14:10 UTC