set intersection

Stream: general

[petercommand]

I am trying to understand the has_Inf instance of submodule defined at https://github.com/leanprover/mathlib/blob/master/linear_algebra/basic.lean#L240
How does the carrier definition work?

[petercommand]

⋂ s ∈ S, ↑s

[petercommand]

I am not sure how it's desugared or how this definition works

[Kenny Lau]

it is ⋂ s, ⋂ H : s ∈ S, ↑s

[petercommand]

H?

[petercommand]

you mean ⋂ s, ⋂ S : s ∈ S, ↑s?

[Kenny Lau]

no, I mean what I typed

[Kenny Lau]

also ⋂ s : submodule α β, ⋂ H : s ∈ S, ↑s