Novice questions on style and structure

Stream: mathlib4

[Jasper Mulder-Sohn]

Hi, for Carleson upstreaming I am looking for some advice on how to approach things and what the preference/etiquette is, before spending time on a PR that might end up wasted.

1. There are the two following forms:

• In Data/Set/Pairwise/Lattice.lean:

theorem pairwise_sUnion {r : α → α → Prop} {s : Set (Set α)} (h : DirectedOn (· ⊆ ·) s) :
    (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, Set.Pairwise a r

• In Data/Set/Lattice.lean:

theorem pairwise_iUnion₂ {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S)
    (r : α → α → Prop) (h : ∀ s ∈ S, s.Pairwise r) : (⋃ s ∈ S, s).Pairwise r

• Is the former (stronger) statement indeed preferred? And should the latter be moved to the former file?
• If so, what is the procedure for making that change? Can I just change the statement and announce a (trivial) breaking change? And how to go about moving the declaration?

2. My original aim is to transfer these results to IsChain (for the subset relation) through a trivial application of IsChain.directedOn.

• Is that considered useful?
• Does a new file Data/Set/Pairwise/Chain.lean sound like a natural place for that? #find_home suggests Order/CompleteLatticebut that only contains the Hausdorff maximality principle at the moment.

Apologies if these questions are elementary and especially if I could have found the answers somewhere in the docs; I did try...

[Ruben Van de Velde]

These are different unions, right?

[Jasper Mulder-Sohn]

Yes they are different but comparable results, but the one is stated as implication and the other as iff

[Jasper Mulder-Sohn]

In both cases the iff result is true

[Ruben Van de Velde]

Okay, then I think we should have the iff for both. I think it's probably fine to replace the existing lemma; it should be easy to adapt any downstream consumers to that

[Ruben Van de Velde]

I don't have an opinion on moving things around right now

[Aaron Liu]

Having an iff is slightly more annoying since you have to put parens (the exception is when there are no explicit arguments before the iff)

[Jasper Mulder-Sohn]

Aaron Liu said:

Having an iff is slightly more annoying since you have to put parens (the exception is when there are no explicit arguments before the iff)

For this you can use the |> pipe operator in most cases, right?

[Jasper Mulder-Sohn]

NB. I would also be happy about some input on question 2 :slight_smile:

[Michael Rothgang]

Iff one direction of the iff is commonly used, you can also have both the iff and just the common direction.

[Jasper Mulder-Sohn]

Michael Rothgang said:

Iff one direction of the iff is commonly used, you can also have both the iff and just the common direction.

I'll go with this, the least controversial option. Then someone else with more stance in the community may follow up if so desired.
I'll also create the new file as that seems the obvious thing to do. Thanks for your input. I will refer to this thread in the PR.

[Eric Wieser]

Michael Rothgang said:

Iff one direction of the iff is commonly used, you can also have both the iff and just the common direction.

Often this is done by proving the Iff, and then using alias to create a shorthand for one direction

[Michael Rothgang]

Or you can prove the common direction first, and then use that in the proof of the iff. (If the "common direction" proof is a bit longer, this can be nicer. If both directions have short proofs, the iff can be nicer. And in general, probably both ways are fine.)

[Jasper Mulder-Sohn]

PR is up: #28119. Thanks for your input!