MulAction.image_iInter

Stream: Is there code for X?

[Alex Kontorovich]

I couldn't find something like this in the library? We have Set.image_iInter and MulAction.bijective but I'm struggling to put them together...? (The below isn't even type-checking for me??) Thanks!

import Mathlib.GroupTheory.GroupAction.Basic

theorem MulAction.image_iInter {α : Type _} {β : Type _} {ι : Type _} [Group α]
    [MulAction α β] (a : α) (s : ι → Set β) :
    a • (⋂ (i : ι), s i) = ⋂ (i : ι), a • s i := sorry

[Eric Wieser]

open scoped Pointwise will help

[Yaël Dillies]

Pretty sure we have it. You guessed the name wrong, though. Let's try docs#Set.smul_set_iInter or docs#Set.smulSet_iInter

[Yaël Dillies]

Hmm, it's not there. But I definitely wrote that lemma, so it must be in one of my branches along with other interesting lemmas.

[Yaël Dillies]

I can open a PR in four days.

[Eric Wieser]

In the meantime:

import Mathlib.GroupTheory.GroupAction.Basic

open scoped Pointwise

theorem Set.smulSet_iInter {α : Type _} {β : Type _} {ι : Sort _} [Group α]
    [MulAction α β] (a : α) (s : ι → Set β) :
    a • (⋂ (i : ι), s i) = ⋂ (i : ι), a • s i :=
  Set.image_iInter (MulAction.toPerm a).bijective _

[Anatole Dedecker]

Interestingly we have the binary version docs#Set.smul_set_inter

[Alex Kontorovich]

Thanks! May I ask, what does open scoped Pointwise do? (I've seen scoped before; don't know what it's for?)

[Eric Wieser]

It means "run all the commands in mathlib that are scoped[Pointwise] foo"

[Eric Wieser]

Which in this particular case is with foo as attribute [instance] someDef

[Kevin Buzzard]

If you ever saw open_locale in lean 3 it's the same sort of thing. It might give you access to things like notation or instances which for some reason you don't want switched on in general. The reasons why we might not want them switched on across mathlib might be lost in the midsts of time -- for example I have absolutely no idea why we still have to open BigOperators before being able to access the standard sigma notation for sums.

[Alex Kontorovich]

Thanks, I feel better! :)