## Stream: general

### Topic: naming contest

#### Anne Baanen (Oct 16 2020 at 15:11):

Any suggestions for a conciser name?

lemma is_basis_to_matrix_mul_linear_map_to_matrix_mul_is_basis_to_matrix
(hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
hc.to_matrix c' ⬝ linear_map.to_matrix hb' hc' f ⬝ hb'.to_matrix b = linear_map.to_matrix hb hc f := sorry


#### Eric Wieser (Oct 16 2020 at 15:24):

Can that be split into two lemmas?

lemma is_basis_to_matrix_mul_linear_map_to_matrix
(hb : is_basis b) (hb' : is_basis b') (hc : is_basis c) (hc' : is_basis c') :
hc.to_matrix c' ⬝ linear_map.to_matrix hb' hc' f = linear_map.to_matrix hb' hc f := sorry


and a similar linear_map_to_matrix_mul_is_basis_to_matrix?

Or am I missing something there?

#### Anne Baanen (Oct 16 2020 at 15:26):

Ah good point, I was thinking about how to describe "basis change" in Lean.

#### Anne Baanen (Oct 16 2020 at 15:26):

But we can do it one side at a time.

#### Anne Baanen (Oct 16 2020 at 15:27):

Still quite a long name :/

#### Gabriel Ebner (Oct 16 2020 at 16:09):

You could turn one of the underscores into a dot and put it in the is_basis namespace.

#### Gabriel Ebner (Oct 16 2020 at 16:10):

Eric's version also looks like a good simp lemma.

#### Yury G. Kudryashov (Nov 07 2021 at 18:54):

I'm going to review API around null_measurable, and I need 4 names:

• null measurable set;
• null measurable function;
• the measurable_space structure that corresponds to null_measurable_set;
• the type tag for "α with measurable_set = null_measurable_set".
For the first two, null_measurable_set and null_measurable look like obvious choices. What about the other two?

#### Sebastien Gouezel (Nov 07 2021 at 19:15):

Just for the record, I know that we need a refactor of the Bochner integral (and I'm planning to do it in a few months, when I have just a little bit of free time), for the following reason. Currently, our version only works when the target space is second countable (this is the setting in which every measurable function can be approximated by simple functions). However, there is a very important application of integral where this is not the case: if you consider a continuous linear operator on a Banach space, then its spectral projections are defined by Cauchy-like integral formulas, so we need integrals there -- and such spaces of operators are never second-countable.

The most general setting to define the integral of a function f is to assume that there is a measurable function g, taking its values in a second-countable subspace, and coinciding almost everywhere with f. (see https://en.wikipedia.org/wiki/Bochner_measurable_function). The name for this would probably be strongly_ae_measurable, or something like that. And it covers the use-case above of spectral projections. So I am planning to generalize the Bochner integral, replacing the ae_measurable assumption with strongly_ae_measurable (which coincides with ae_measurable when the target space is second-countable).

This does not really answer your questions, but I think this is something to keep in mind for any measure theory API review.

#### Sebastien Gouezel (Nov 07 2021 at 19:19):

As for your questions, null_measurable_set is great. null_measurable is ok for the function (but in the end it is equivalent to ae_measurable, so I am not so sure we need the two names). Then, you could go with measurable_space_completion μ for the completed sigma-algebra, and is_complete_measurable_space μ for the fact that all null measurable sets are measurable (as in https://en.wikipedia.org/wiki/Complete_measure)

#### Yury G. Kudryashov (Nov 07 2021 at 19:51):

In what generality null_measurable = ae_measurable?

#### Yury G. Kudryashov (Nov 07 2021 at 19:53):

In any case, I think that we should have better API for null_measurable_sets.

#### Sebastien Gouezel (Nov 07 2021 at 21:16):

Yury G. Kudryashov said:

In what generality null_measurable = ae_measurable?

I guess when the target space is second-countable.

#### Sebastien Gouezel (Nov 07 2021 at 21:16):

Yury G. Kudryashov said:

In any case, I think that we should have better API for null_measurable_sets.

Yes, definitely!

#### Andrew Yang (Dec 02 2021 at 02:45):

What should the pasting law for pullbacks be called?
In particular

variables {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ X₂) (g₁ : X₂ ⟶ X₃) (f₂ : Y₁ ⟶ Y₂) (g₂ : Y₂ ⟶ Y₃)
variables (i₁ : X₁ ⟶ Y₁) (i₂ : X₂ ⟶ Y₂) (i₃ : X₃ ⟶ Y₃)
variables (h₁ : i₁ ≫ f₂ = f₁ ≫ i₂) (h₂ : i₂ ≫ g₂ = g₁ ≫ i₃)

def pasting_law (H : is_limit (pullback_cone.mk _ _ h₂)) :
is_limit (pullback_cone.mk _ _ (show i₁ ≫ f₂ ≫ g₂ = (f₁ ≫ g₁) ≫ i₃,
by rw [← category.assoc, h₁, category.assoc, h₂, category.assoc])) ≃
is_limit (pullback_cone.mk _ _ h₁) := sorry


And the implications in both directions that will be proved before this.

#### Yury G. Kudryashov (Dec 03 2021 at 11:01):

I'm going to add Prop versions of docs#fintype and docs#encodable. How should I call them?

#### Johan Commelin (Dec 03 2021 at 11:17):

_root_.finite and _root_.countable?

#### Mario Carneiro (Dec 03 2021 at 11:23):

doesn't docs#countable already exist? guess not

#### Kevin Buzzard (Dec 03 2021 at 22:49):

Funnily enough an undergraduate and I wrote _root_.countable at Xena on Thursday but it's on the student's laptop and I don't know their name :-)

#### Yury G. Kudryashov (Dec 03 2021 at 23:36):

I already have _root_.countable with some instances. I'll add glue code and PR it over week-end.

#### Yury G. Kudryashov (Feb 20 2022 at 04:06):

I'm going to formalize a few versions of the Phragmén–Lindelöf principle. Mathlib naming convention leads to very long names. What do you think about names like phragmen_lindelof.(shape), where (shape) is one of sector, first/second/third/fourth_quadrant etc?

#### Yury G. Kudryashov (Feb 20 2022 at 04:06):

(and now I see that I forgot to polish _root_.countable)

#### Sebastien Gouezel (Feb 20 2022 at 09:32):

Looks good to me.

#### Eric Wieser (Mar 06 2022 at 16:47):

What should the additive version of div_inv_monoid be called? docs#sub_neg_monoid exists, but @[to_additive] thinks it should be called sub_neg_add_monoid, as demonstrated by docs#function.injective.sub_neg_add_monoid.

#### Eric Wieser (Mar 06 2022 at 16:49):

/poll With or without add_?

• sub_neg_monoid, keeping the existing class name and fixing to_additive to match

#### Eric Wieser (Mar 06 2022 at 16:49):

cc @Anne Baanen, since I think you added this originally

#### Junyan Xu (Mar 18 2022 at 08:19):

/poll What should $V^G$ be called for a G-representation V? (Context)

• fixed_space
• invariants

#### Kevin Buzzard (Mar 18 2022 at 08:35):

cohomology.H 0 G V ;-) (this is not a correct answer -- there should probably just be an isomorphism...)

#### Reid Barton (Mar 18 2022 at 10:19):

invariants seems good also because the dual guy is called the coinvariants (what else?)

#### Yury G. Kudryashov (Apr 21 2022 at 22:39):

How should I call the following lemmas?

import data.set.finite

open set
variables {α β ι : Type*} [fintype ι] {π : ι → Type*}

example {s : set (α × β)} : finite s ↔ finite (prod.fst '' s) ∧ finite (prod.snd '' s) :=
⟨λ h, ⟨h.image _, h.image _⟩,
λ h, (h.1.prod h.2).subset $λ x h, ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩⟩ example {s : set (Π i, π i)} : finite s ↔ ∀ i, finite (eval i '' s) := ⟨λ h i, h.image _, λ h, (finite.pi h).subset$ subset_pi_eval_image _ _⟩


#### Yury G. Kudryashov (Apr 21 2022 at 23:34):

Probably, the name of the first lemma should include finite and prod. There is also a reasonable lemma

example {s : set α} {t : set β} : finite (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ finite s ∧ finite t


#### Eric Wieser (Apr 22 2022 at 05:58):

set.finite_of_prod_iff, using the rule "of refers to the type of arguments"?

#### Yaël Dillies (Apr 22 2022 at 07:31):

I would name the third one set.prod_finite_iff.

#### Floris van Doorn (Apr 22 2022 at 11:15):

of sounds weird to me, since it's the type we're talking about.
I like set.finite_prod_iff for both the first and the third one, and I'm not sure how to best disambiguate them. Both of them are follow the example of existing names. E.g. docs#measurable_pi_iff , docs#measurable_prod for the first one, and docs#set.finite_union / docs#filter.tendsto_prod_iff for the other one (we seem to be quite inconsistent about whether to append iff to a name).

#### Eric Wieser (Apr 22 2022 at 11:37):

Well, when we usually use of for proofs, it also refers to the type

#### Eric Wieser (Apr 22 2022 at 11:37):

I think we also sometimes use docs#of_fintype in names, which is referring to a non-Prop type

#### Yury G. Kudryashov (Apr 23 2022 at 00:39):

In #13619 I swap LHS with RHS and describe the new LHS in the name. Not sure if it is a good solution.

#### Yury G. Kudryashov (May 16 2022 at 15:58):

How should I call the following definition?

def name_me (f : α → β → γ) : option α → option β → option γ
| none none := none
| none (some b) := none
| (some a) none := none
| (some a) (some b) := some (f a b)


Equivalently, name_me f o₁ o₂ = o₁.bind (λ a, o₂.map (f a)).

#### Yury G. Kudryashov (May 16 2022 at 15:59):

How is it called?

#### Yaël Dillies (May 16 2022 at 16:02):

Ah no, I thought it was docs#option.lift_or_get but it doesn't do the same thing when one of the arguments is none.

#### Kyle Miller (May 16 2022 at 16:02):

example {α β γ : Type*} (f : α → β → γ) (x : option α) (y : option β) :

#### Yaël Dillies (May 16 2022 at 16:04):

A good name would be option.map\2 but indeed you can just write it out monadically.

#### Yury G. Kudryashov (May 16 2022 at 16:05):

Yes, I wanted to prove some lemmas about this combinator, then use it for (+) and (*) on with_top.

#### Yaël Dillies (May 16 2022 at 16:05):

Yeah... but if we perform the functor refactor we talked about, that wouldn't be a problem anymore.

#### Eric Wieser (May 16 2022 at 16:05):

it was never clear to me whether that refactor would actually work

#### Kyle Miller (May 16 2022 at 16:06):

(n.b. this uses the weaker notion of an applicative functor, no need for monads)

#### Yaël Dillies (May 16 2022 at 16:06):

What are you fearing? I thought about it and couldn't see anything wrong.

#### Eric Wieser (May 16 2022 at 16:06):

Typeclass search not handling out_params well enough

#### Yaël Dillies (May 16 2022 at 16:06):

Yury, Yakov already wanted to do that, and it turns out that this is not a good global instance because sometimes you want the top element to not do anything

#### Yaël Dillies (May 16 2022 at 16:07):

Let me dig out the PR...

#### Yaël Dillies (May 16 2022 at 16:09):

Ah right, it was subtraction. #8889

#### Mauricio Collares (May 16 2022 at 16:10):

I'd expect something close to Haskell's naming (liftA\2)

#### Anne Baanen (May 16 2022 at 16:10):

For the name, I would follow Haskell and use some variant of lift2

#### Yaël Dillies (May 16 2022 at 16:11):

Yeah so 0 * top = 0, not 0 * top = top.

#### Yury G. Kudryashov (May 16 2022 at 16:12):

Yes, lift₂ will be used for the else branch.

#### Violeta Hernández (Jun 22 2022 at 04:41):

We currently have two duplicate theorems docs#set.insert_nonempty and docs#set.nonempty_insert. My PR #14884 is meant to ditch one in favor of the other, but I was asked to do a poll to see which one is preferred.

Consider that:

#### Violeta Hernández (Jun 22 2022 at 04:43):

/poll What name should we use?

• insert_nonempty
• nonempty_insert

#### Kyle Miller (Jun 22 2022 at 04:47):

This is the old debate about whether the naming for p x is x_p when p is a Prop-valued predicate that is amenable to dot notation, and, as far as I know, we haven't reached consensus about this yet. It would be nice to have #naming prescribe something.

#### Kyle Miller (Jun 22 2022 at 04:50):

Maybe this is a decision that can be made per predicate and documented in the predicate's docstring. It seems (though I haven't measured) that set.nonempty most often uses the *_nonempty convention.

#### Violeta Hernández (Jun 22 2022 at 04:53):

I also think this decision should be made on a per-predicate basis. I'd be somewhat annoyed if I had to rename e.g. one_to_game to to_game_one (example from one of my PRs). No doubt there's a similar situation going the other way (though I'm awful at coming up with examples for things like this).

#### Eric Wieser (Jun 22 2022 at 11:58):

Just to relink the old thread on this type of naming issue: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.23naming.20and.20dot.20notation/near/246520191

#### Eric Wieser (Jun 22 2022 at 11:59):

For what it's worth, I'd expect it to be called to_game_one to match all the coe_one lemmas we have

#### Violeta Hernández (Jun 22 2022 at 12:39):

Unfortunate but understandable

#### Stuart Presnell (Jul 02 2022 at 09:01):

#15061 adds two recursion principles for P : ℕ → ℕ → Sort* for which I'm looking for naming suggestions:

• strong_sub_recursion: if for all a b : ℕ we can extend P from the rectangle strictly below (a,b) to P a b, then we have P n m for all n m : ℕ.
This was originally proved and named by @Chris Birkbeck in #14828 (which is now closed)

• pincer_recursion: if we have P i 0 and P 0 i for all i : ℕ, and for any x y : ℕ we can extend P from (x,y+1) and (x+1,y) to (x+1,y+1), then we have P n m for all n m : ℕ.
pincer_recursion is just a name I made up for this. Does anyone know if this is already known by another name? Or can anyone suggest a better name for this?

#### Stuart Presnell (Jul 03 2022 at 18:19):

Another naming question: #15072 defines multichoose which (by contrast with choose) counts the number of multisets of cardinality k from a type of cardinality n, or equivalently the number of ways to select k items (up to permutation) from n items with replacement. (This is another step toward getting @Huỳnh Trần Khanh's #11162 "stars and bars" tidied up and finalised.)

Some reviewers have suggested that the name multichoose (which I took from #11162) is a problem because it wrongly suggests multinomial coefficients. The alternative name multicombination has been suggested. Does anyone have a strong preference for either of these names, or another suggestion?

#### Kyle Miller (Jul 03 2022 at 18:25):

According to https://mathworld.wolfram.com/Multichoose.html multichoose should be fine for this.

#### Kyle Miller (Jul 03 2022 at 18:27):

Another way to justify the name is that where choose is choosing things singly, multichoose is choosing things with multiplicity.

#### Kyle Miller (Jul 03 2022 at 18:27):

In the doc string, it'd be good to mention that multichoose is also known as counting multicombinations (and have multicombination in the module doc's tags), if you haven't already.

#### Kyle Miller (Jul 03 2022 at 18:29):

May as well put in a hint that this is not the multinomial coefficient, too.

#### Kyle Miller (Jul 03 2022 at 18:34):

As a counterpoint, https://www.rdocumentation.org/packages/iterpc/versions/0.4.2/topics/multichoose is the multinomial coefficient, but this library seems to be unique in calling it that. "Multichoose" seems to be this PR's multichoose everywhere else.

#### Eric Wieser (Jul 03 2022 at 18:47):

Maybe add a reference to Wolfram for the naming in the docstring, just to be extra safe?

#### Violeta Hernández (Jul 04 2022 at 00:13):

Yeah, if the docs make it clear enough that this name is used elsewhere and not the multinomial coefficient, then I completely support it

#### Violeta Hernández (Jul 17 2022 at 23:12):

We have docs#cardinal.mk_set_le_aleph_0 and docs#cardinal.lt_aleph_0_iff_set_finite. These are very similar statements but have very different names.

#### Violeta Hernández (Jul 17 2022 at 23:14):

The only other related lemma with a similar name to the former is docs#cardinal.mk_subtype_le_aleph_0, while there's a few other lemmas about finite sets with similar names to the latter, such as docs#cardinal.lt_aleph_0_iff_finite and docs#cardinal.lt_aleph_0_of_finite.

#### Violeta Hernández (Jul 17 2022 at 23:16):

I would much prefer to be consistent, particularly since we'll be adding a bunch more very similar lemmas now that we have our new docs#countable typeclass. So I might as well put it up to vote.

#### Violeta Hernández (Jul 17 2022 at 23:17):

/poll Which scheme should we prefer for these lemmas?

• mk_set_le_aleph_0
• lt_aleph_0_iff_set_finite
• other (suggest)

#### Violeta Hernández (Jul 17 2022 at 23:18):

I marginally prefer the lt_aleph_0_iff_set_finite scheme, since it allows us to clearly distinguish between the iff versions and the one sided versions of these lemmas.

#### Yury G. Kudryashov (Jul 19 2022 at 02:26):

We have duplicate definitions: docs#equiv.nat_prod_nat_equiv_nat vs docs#nat.mkpair_equiv.

#### Yury G. Kudryashov (Jul 19 2022 at 02:26):

/poll Which name should stay in mathlib?
equiv.nat_prod_nat_equiv_nat
nat.mkpair_equiv
I don't care

#### Yury G. Kudryashov (Jul 19 2022 at 02:27):

I want to remove one of the names, no matter which one.

#### Yury G. Kudryashov (Jul 19 2022 at 02:34):

See #15509 and #15510 for PRs implementing different options.

#### Junyan Xu (Jul 19 2022 at 02:39):

There are many possible equivalences between ℕ × ℕ and ℕ, and the name equiv.nat_prod_nat_equiv_nat doesn't specify which one it is. Since the to_fun and inv_fun are already named docs#nat.mkpair and docs#nat.unpair, it's better to include (at least one of) these in the name.

#### Yury G. Kudryashov (Jul 19 2022 at 12:16):

It looks like nat.mkpair_equiv wins.

#### Jireh Loreaux (Jul 22 2022 at 14:47):

In case anyone didn't see the poll hidden in the other thread and wants to vote (about nondiscrete normed field), please read the summary post immediately prior to the poll: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/hypotheses.20for.20a.20field.20property/near/290408091

#### Jireh Loreaux (Aug 04 2022 at 20:10):

I think the naming for continuous_linear_map.lmul and friends is weird. It doesn't match the non-continuous version (which had some recent changes in #15310). Before #15310, continuous_linear_map.lmul was defined in terms of algebra.lmul (and I'm fairly certain that the "l" is for "linear", because the docstring used to call it a bilinear map, even though it was an algebra hom), and I believe this is why it was named as such.

In any case, we used to have algebra.lmul_left and algebra.lmul_right (now named linear_map.mul_left and linear_map.mul_right), but continuous_linear_map.lmul_right does not correspond to linear_map.mul_right and continuous_linear_map.lmul_left doesn't even exist. So, I think the things in the continuous_linear_map namespace should be renamed appropriately. My feeling is:

1. continuous_linear_map.lmulcontinuous_linear_map.mul
2. continuous_linear_map.lmul_rightcontinuous_linear_map.mul_flip (or just delete this if it's not frequently used; it's literally defined as (continuous_linear_map.mul _ _).flip)
3. continuous_linear_map.lmul_left_rightcontinuous_linear_map.mul_mul

#### Jireh Loreaux (Aug 05 2022 at 16:58):

I think maybe people missed this yesterday.

#### Jireh Loreaux (Aug 22 2022 at 16:12):

In #16161 I am making equiv_like extend fun_like, and to do so we must rename the current coe_injective' field to something else. Currently in the PR it has been renamed to coe_inv_injective' (the type is ∀ e g : E, coe e = coe g → inv e = inv g → e = g). However, @Anne Baanen mentioned that this seems wrong, but can't think of anything better. Hence poll:

#### Jireh Loreaux (Aug 22 2022 at 16:13):

/poll the field equiv_like.coe_injective' should be renamed to:
coe_inv_injective'
ext'
eq_of_coe_eq_of_inv_eq

#### Oliver Nash (Aug 22 2022 at 19:27):

I completely agree with Anne's remark here so I don't love coe_inv_injective' but it is definitely the least bad of the various possibilities I can think of.

#### Praneeth Kolichala (Sep 01 2022 at 18:41):

Here, I defined polynomial time functions using the native datatype ptree ("plain binary tree"). This is because mathlib's mkpair encoding causes exponential blowup in e.g. the encoding of lists. At some point, I will try porting this to mathlib. In addition, the entire computability library should, I believe, be refactored to use this datatype, because it is the most direct representation of what we actually want to represent -- namely tree structures. I've already discussed this a bit with @Mario Carneiro .

What should this data structure be called:

inductive ptree
| nil
| node (left : ptree) (right : ptree)


#### Praneeth Kolichala (Sep 01 2022 at 18:43):

/poll What to call a plain binary tree
ptree
plain_tree
binary_tree

#### Yaël Dillies (Sep 01 2022 at 20:51):

I assume this is the same as tree unit?

#### Praneeth Kolichala (Sep 01 2022 at 20:57):

Yaël Dillies said:

I assume this is the same as tree unit?

Yes, I think so

#### Junyan Xu (Sep 01 2022 at 22:01):

You could also use docs#free_magma unit right?

#### Bolton Bailey (Sep 02 2022 at 02:26):

I don't like binary_tree because it implies that tree isn't binary.

#### Bolton Bailey (Sep 02 2022 at 02:28):

In fact, it's a bit unfortunate that we have both docs#bin_tree and docs#tree and the difference isn't that one is binary and the other is not the difference is in how leaves are represented. Edit: I guess this is due to the former being in core

Last updated: Aug 03 2023 at 10:10 UTC