Non-simp-normal forms in definitions/lemmas

Stream: mathlib4

[Yury G. Kudryashov]

Some definitions like src#Set.image2 and src#IsCompact use non-simp-normal assumptions (∃ y, x ∈ s ∧ _ instead of x ∈ s ∧ ∃ y, _ and f ≤ 𝓟 s instead of s ∈ f, respectively). Should we change them and/or discourage this style?

[Yaël Dillies]

I've been meaning to replace docs#Set.image2 and docs#Convex but never got around to doing it. It's not worth changing the latter since I'll be doing the convexity refactor anyway, but the former should be done.

[Patrick Massot]

I strongly prefer to keep isCompact in this intuitive form.

[Yury G. Kudryashov]

What about API lemmas for IsCompact?

[Patrick Massot]

Which lemmas?

[Yury G. Kudryashov]

E.g., docs#IsCompact.adherence_nhdset

[Yury G. Kudryashov]

Or docs#isCompact_iff_ultrafilter_le_nhds (see the primed version below for a simp-normal form)

[Yury G. Kudryashov]

Other example of _ ≤ 𝓟 _ in assumptions: docs#IsPreconnected.intermediate_value₂_eventually₁ and the next several lemmas.

[Patrick Massot]

I would keep them. I don't see the point in making statements harder to read

[Yury G. Kudryashov]

I guess, we have different intuition here.

[Patrick Massot]

I think the proper fix is to change our simp normal form here. The intuitive meaning of "F le principal s" is simply that the generalized set F is contained in the ordinary set s.

[Yury G. Kudryashov]

Let's postpone this discussion till after the New Year.

[Yury G. Kudryashov]

If we simplify s ∈ f to f ≤ principal s, then there is no reason to have ∈ notation at all.