Define relative rank of matroids

Stream: mathlib4

[Martin Dvořák]

How would you improve the following definition of relative rank of matroids?

import Mathlib.Data.Matroid.IndepAxioms

noncomputable def IndepMatroid.relativeRank {α : Type*} {A B : Set α}
    (M : IndepMatroid α) (hA : A ⊆ M.E) (hB : B ⊆ A) :
    ℕ∞ :=
  ⨆ (J : {_J // _J ∈ maximals Set.Subset {X | M.Indep X ∧ X ⊆ B}}),
    ⨆ (I : {_I // M.Indep _I ∧ _I ⊆ A ∧ J.val ⊆ _I}),
      Set.encard (I.val \ J.val)

We @Ivan S. find this definition very hard to work with.

If you want to read the definition written in LaTeX, see it on top of page 2 here:
https://github.com/madvorak/matroids/blob/master/theory/theory.pdf

[Kyle Miller]

You can avoid working with subtypes by working with nested suprema. You can also omit hA and hB since they're not used (the principle being "it's up to theorems to make sure definitions are used in their intended domains"), unless there are some simp lemmas where it's essential to have these facts available in the expression.

noncomputable def IndepMatroid.relativeRank {α : Type*} {A B : Set α}
    (M : IndepMatroid α) : -- (hA : A ⊆ M.E) (hB : B ⊆ A) :
    ℕ∞ :=
  ⨆ J ∈ maximals Set.Subset {X | M.Indep X ∧ X ⊆ B},
    ⨆ I, ⨆ _ : M.Indep I ∧ I ⊆ A ∧ J ⊆ I,
      Set.encard (I \ J)

[Eric Wieser]

(a general reminder for other readers:nested suprema are only safe in general on complete lattices; which in this case ENat is!)

[Peter Nelson]

Relative rank is free once you have rank and minors. I've done it all here :
https://github.com/apnelson1/Matroid/blob/main/Matroid/Minor/RelRank.lean

There is quite a large amount of stuff in that repo - it is being written with mathlib in mind, and I think the vast majority is PR-ready - the speed of the review process is part of the reason it's not already there.

I'm very happy to see others working on matroids! but could I politely suggest that you look at some topics not already in my repo? There is still plenty to do. (I realize you may not have been aware of it earlier).

[Peter Nelson]

This has motivated me to make start on my next matroid PR!

[Martin Dvořák]

Peter Nelson said:

Relative rank is free once you have rank and minors. I've done it all here :
https://github.com/apnelson1/Matroid/blob/main/Matroid/Minor/RelRank.lean

There is quite a large amount of stuff in that repo - it is being written with mathlib in mind, and I think the vast majority is PR-ready - the speed of the review process is part of the reason it's not already there.

I'm very happy to see others working on matroids! but could I politely suggest that you look at some topics not already in my repo? There is still plenty to do. (I realize you may not have been aware of it earlier).

Thanks for letting us know! We certainly don't want to duplicate the work you already did or compete against you. Do you have a roadmap of things about matroids you want to formalize? Please feel free to comment on our work in progress here:
https://github.com/madvorak/matroids
We will be happy to receive comments even before we PR parts of our work to Mathlib.

@Ivan S.