Zulip Chat Archive

Stream: general

Topic: set intersection


petercommand (Nov 18 2018 at 07:56):

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 (Nov 18 2018 at 07:56):

⋂ s ∈ S, ↑s

petercommand (Nov 18 2018 at 07:56):

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

Kenny Lau (Nov 18 2018 at 09:04):

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

petercommand (Nov 18 2018 at 09:36):

H?

petercommand (Nov 18 2018 at 09:36):

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

Kenny Lau (Nov 18 2018 at 09:37):

no, I mean what I typed

Kenny Lau (Nov 18 2018 at 09:38):

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


Last updated: Dec 20 2023 at 11:08 UTC