## Stream: maths

### Topic: Lemma naming contest

#### Patrick Massot (Sep 28 2020 at 15:07):

Heather and I need help to name lemmas (or find them already named in mathlib).

lemma inf_property' {α : Type*} [ordered_add_comm_group α] {s : set α} {a ε : α}
(h₁ : is_glb s a) (h₂ : a ∉ s) (h₃ : 0 < ε) : ∃ b, b ∈ s ∧ a < b ∧ ¬ a + ε ≤ b :=
sorry

lemma inf_property {α : Type*} [decidable_linear_ordered_add_comm_group α] {s : set α} {a ε : α}
(h₁ : is_glb s a) (h₂ : a ∉ s) (h₃ : 0 < ε) : ∃ b, b ∈ s ∧ a < b ∧ b < a + ε :=
by simpa using inf_property' h₁ h₂ h₃


The proof is omitted for brevity, we had no trouble proving this. @Scott Morrison: enjoy the type class mess in these examples, in relation to our previous discussion.

#### Rob Lewis (Sep 28 2020 at 15:12):

is_glb.exists_lt_mem?

#### Patrick Massot (Sep 28 2020 at 15:14):

To me it sounds like a pretty random sampling from the statement, but if you like it then it's good enough for me.

#### Rob Lewis (Sep 28 2020 at 15:16):

It is exactly that, but most options will be unless you spell everything out. is_glb.exists_lt_mem_near?

#### Patrick Massot (Sep 28 2020 at 15:18):

And we have two lemmas to name.

#### Patrick Massot (Sep 28 2020 at 15:18):

TBH I don't expect the first one will get any use, maybe I should remove it.

#### Patrick Massot (Sep 28 2020 at 15:19):

Heather originally stated this for real numbers and I simply picked random type classes to make it look more respectable;

#### Reid Barton (Sep 28 2020 at 15:29):

is_glb.exists_between_self_add?

#### Reid Barton (Sep 28 2020 at 15:29):

Or exists_lt_add

#### Kevin Buzzard (Sep 28 2020 at 15:30):

Life was so much easier when we could just call it lemma 37.

#### Yury G. Kudryashov (Sep 28 2020 at 16:07):

Kevin Buzzard said:

Life was so much easier when we could just call it lemma 37.

Like in some parts of coq stdlib?

#### Kevin Buzzard (Sep 28 2020 at 16:21):

imagine trying to use the API :-) I was skeptical of this naming system at first, believing it simply would not scale. But often I realised one just had to break things down carefully into the right pieces and name them well.

#### Patrick Massot (Sep 28 2020 at 21:13):

Ok, I went with a variation on Reid's proposal. Next challenge is: where should we put:

lemma add_subgroup.int_mul_mem {R : Type*} [ring R] {G : add_subgroup R} (k : ℤ) {g : R} (h : g ∈ G) :
(k : R) * g ∈ G :=
begin
convert add_subgroup.gsmul_mem G h k,
exact (gsmul_eq_mul g k).symm,
end


#### Patrick Massot (Sep 28 2020 at 21:14):

This needs both ring and add_subgroup.

#### Heather Macbeth (Sep 28 2020 at 21:16):

@Patrick Massot Actually, I was wondering if the branch could be rewritten to use only k •ℤ g.

#### Heather Macbeth (Sep 28 2020 at 21:17):

I can try this later if you like the idea.

#### Patrick Massot (Sep 28 2020 at 21:17):

Maybe. I think the lemma is good to have anyway. It's bedtime here, so it's your turn to play with this branch. I think this lemma is the last remaining thing to move.

Last updated: May 12 2021 at 08:14 UTC