Function inequalities

Stream: general

[Bhavik Mehta]

Do we have a convention on whether p ≤ q or ∀ a, p a ≤ q a is the preferred spelling? Of course I think we should have both in most cases, but is there something written down somewhere, and if not do people have an idea which is used more commonly in mathlib? (This came up in https://github.com/leanprover-community/mathlib/pull/14827#discussion_r904064035)
(edited to clarify what I'm actually interested in asking)

[Eric Wieser]

The fact that we have three different notations for le (→, ⊆, ≤) makes it all a bit unclear regarding which spelling is preferred

[Eric Wieser]

Although I think the elaborator often struggles for le on pi types, as f ≤ g is a function in a way that x ≤ y usually isn't

[Bhavik Mehta]

True, I suppose what I'm actually interested in is the case p ≤ q vs ∀ a, p a ≤ q a; the linked PR talks about p ≤ q vs ∀ a, p a ⊆ q a, which itself here can be written ∀ a x, x ∈ p a → x ∈ q a

[Eric Wieser]

That last spelling (with p a x →q a x) is banned, it abuses sets

[Eric Wieser]

∀ a x, x ∈ p a → x ∈ q a is ok

[Bhavik Mehta]

oops, corrected

[Eric Wieser]

I think for sets it's pretty clear that ⊆ is preferred vs unfolding all the way

[Eric Wieser]

The problem with using h : p ≤ q is that it expands as h a : p a ≤ q a instead of p a ⊆ q a, which isn't the form we normally use. Now, if we eliminated ⊆ notation...

[Bhavik Mehta]

In the case of sets or finsets, at least

[Eric Wieser]

To be clear, your example above is p q : α → set β, right?

[Bhavik Mehta]

Exactly, yes