Precedence of image/preimage notation

Stream: mathlib4

[Robert Maxton]

Given how '' and ⁻¹' are generally used -- as infix notations that are frequently chained, where e.g. f '' (g '' x) = (g ∘ f) '' x -- wouldn't they make more sense as infixrs, so that we don't have to add so many extra parentheses?

[Alex Meiburg]

You mean you never associate it the other way?

example (myfs : Set (ℕ → ℕ)) (h : myfs = {(· + 13), (· * 4)}) :
     (·^[2]) '' myfs '' {(· + 26)} = { True } := by
  ext; simp [h, Set.image, setOf]; rfl

[Robert Maxton]

No, and in fact that application is syntactically limited in that you can only have as many associations as the function type you start with has variables, whereas I am currently working in a case where I have a solid four 'swaps' between preimages and images
(Hidden to some extent by API and intermediate lemmas, but it still comes up sometimes)

[Robert Maxton]

I feel like "times when you apply/inverse-apply $n$ functions to sets" are going to be inherently more common than "times when you're dealing with sets of $n$-ary functions"

[Alex Meiburg]

Yes, I was absolutely joking, I agree it should associate the other way. :slight_smile: Sorry, humor doesn't go so well over text I guess!

[Robert Maxton]

ah lmao, fair enough
(That's what emojis are for! xP)

[Aaron Liu]

(you can't associate the other way without defeq abuse)

[Robert Maxton]

eh?

[Aaron Liu]

Since the output is a set and the left input is a function anything left-associative (the current default) will be defeq abuse of the fact the sets are defined as functions to Prop

[Robert Maxton]

Sorry, I'm still not seeing it:

import Mathlib.Data.Set.Defs

infixr:80 " '' " => Set.image

theorem image_comp (f : α → β) (g : β → γ) (s : Set α) : g '' f '' s = (g ∘ f) '' s := by
  apply Set.ext
  intro x
  constructor <;> (intro h; simp only [Set.image, Function.comp_apply] at h ⊢ )
  · rcases h with ⟨b, ⟨a, ha, rfl⟩, rfl⟩
    refine ⟨a, ha, rfl⟩
  · rcases h with ⟨a, ha, rfl⟩
    refine ⟨f a, ⟨a, ha, rfl⟩, rfl⟩

Where's the defeq abuse here?

[Junyan Xu]

Alex Meiburg said:

Yes, I was absolutely joking, I agree it should associate the other way. :slight_smile: Sorry, humor doesn't go so well over text I guess!

In China they use a dog face emoji like :puppy: for this :) https://chatgpt.com/s/t_68a6f827d48c8191a2db7dd3f93795e6