Lemma naming contest

Stream: maths

[Patrick Massot]

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]

is_glb.exists_lt_mem?

[Patrick Massot]

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]

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

[Patrick Massot]

And we have two lemmas to name.

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

is_glb.exists_between_self_add?

[Reid Barton]

Or exists_lt_add

[Kevin Buzzard]

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

[Yury G. Kudryashov]

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]

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]

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]

This needs both ring and add_subgroup.

[Heather Macbeth]

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

[Heather Macbeth]

I can try this later if you like the idea.

[Patrick Massot]

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.