Finitary matroids

Stream: mathlib4

[Martin Dvořák]

Should
docs#Matroid.indep_of_forall_finite_subset_indep
and
docs#Matroid.indep_iff_forall_finite_subset_indep
be called
Matroid.Finitary.indep_of_forall_finite_subset_indep
and
Matroid.Finitary.indep_iff_forall_finite_subset_indep
instead?

[Martin Dvořák]

Also, could and should

theorem Matroid.finitary_iff_iff {α : Type*} (M : Matroid α) :
  M.Finitary ↔ (∀ I : Set α, (∀ J ⊆ I, J.Finite → M.Indep J) ↔ M.Indep I)

be added to Mathlib?

[Violeta Hernández]

That last one should probably be called Matroid.finitary_iff_forall_iff

[Jihoon Hyun]

I'm pretty sure that only explicit arguments were considered for names of theorems about matroids. If those name were to be fixed then maybe we need a full renaming of theorems.

[Martin Dvořák]

Jihoon Hyun said:

I'm pretty sure that only explicit arguments were considered for names of theorems about matroids.

This is what I usually do. Here, however, the first explicit argument is of the type Set α and I don't think that Set.indep_of_forall_finite_subset_indep should be the name.

[Jihoon Hyun]

Maybe the better solution is to make I implicit.

[Martin Dvořák]

Should M be explicit? Or should h be the only explicit argument?

[Jihoon Hyun]

I suggest M and I implicit and h explicit.

[Martin Dvořák]

If Finitary shouldn't be in the prefix, should the names of the two existing lemmas be
Matroid.indep_of_forall_finite_subset_indep_of_finitary
and
Matroid.indep_iff_forall_finite_subset_indep_of_finitary
instead?

[Martin Dvořák]

@Peter Nelson

[Jihoon Hyun]

Martin Dvořák said:

If Finitary shouldn't be in the prefix, should the names of the two existing lemmas be
Matroid.indep_of_forall_finite_subset_indep_of_finitary
and
Matroid.indep_iff_forall_finite_subset_indep_of_finitary
instead?

I don't think these should be named as you suggested. As I said above, many theorems about matroids only include names of explicit arguments, and Finatary is implicit.

[Ruben Van de Velde]

In any case, you're not required to include all parts included in the naming convention. You just need enough to disambiguate the theorems