Basis "flags" indexed by poset

Stream: Is there code for X?

[Robert Spencer]

I'm looking for a generalisation of Module.Basis.flag which applies to more general posets. For example something along the lines of

variable {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M]
variable (Λ : Type) [PartialOrder Λ] [Fintype Λ] (f : Λ → ℕ)

def Module.Basis.poset_flag (b : Basis (Σ μ, Fin (f μ)) R M) (S : Set Λ) :
  Submodule R M := Submodule.span R (b '' (Sigma.fst ⁻¹' S))