How much tfae

Stream: mathlib4

[Aaron Liu]

What's a reasonable amount of lemmas to have for a TFAE? I'm assuming 17 is too many. Which ones should I keep?

import Mathlib.Topology.Coherent
import Mathlib.Topology.Specialization

theorem alexandrovDiscrete_tfae {X : Type*} [tX : TopologicalSpace X] :
    [
      AlexandrovDiscrete X,
      ∀ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S),
      ∀ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) → IsClosed (⋃₀ S),
      ∀ (x : X) (S : Set (Set X)), (∀ s ∈ S, s ∈ nhds x) → ⋂₀ S ∈ nhds x,
      ∀ (x : X), (nhds x).ker ∈ nhds x,
      ∀ (x : X), IsOpen (exterior {x}),
      ∀ (s : Set X), IsOpen (exterior s),
      tX = @Topology.upperSet X (specializationPreorder X),
      ∃ (p : Preorder X), tX = @Topology.upperSet X p,
      ∃ (p : Preorder X), tX = @Topology.lowerSet X p,
      ∀ (S : Set (Set X)), interior (⋂₀ S) = ⋂ s ∈ S, interior s,
      ∀ (S : Set (Set X)), closure (⋃₀ S) = ⋃ s ∈ S, closure s,
      ∀ (x : X) (S : Set X), x ∈ closure S ↔ ∃ (f : Finset X), f.toSet ⊆ S ∧ x ∈ closure f,
      ∀ (x : X) (S : Set X), x ∈ closure S ↔ ∃ y ∈ S, y ⤳ x,
      ∀ (s : Set X), IsOpen s ↔ ∀ (x y : X), x ⤳ y → y ∈ s → x ∈ s,
      @Topology.IsCoherentWith X tX (setOf Set.Finite),
      ∀ (s : Set X), IsOpen s ↔ ∀ (f : Finset X), IsOpen ((↑) ⁻¹' s : Set f)
    ].TFAE := by
  -- proof omitted
  sorry

[Ruben Van de Velde]

Why is it too many?

[Eric Wieser]

Hot take: you should not use a TFAE here at all

[Eric Wieser]

This should be a series of lemmas of the form alexandrovDiscrete_iff_foo

[Eric Wieser]

(you can use a private tfae internally if it helps you set up the API, but it's not a good interface for referring to the result later)

[Junyan Xu]

Not sure it should be private, it's nice to have it show up in the docs (like it would appear in books)
The tfae tactics are definitely very useful in proving TFAEs.

[Junyan Xu]

I have an issue with putting TFAE at the end; wouldn't that be TAAE instead? If you don't want the List. you can open List (TFAE).

[Aaron Liu]

Eric Wieser said:

Hot take: you should not use a TFAE here at all

It's so I can prove the result without pain, eg. I have a loop 1 → 15 → 8 → 14 → 17 → 2 ↔ 1, so it's easier to get the iff by having the TFAE.

[Eric Wieser]

RIght, that's what I mean by "internally if it helps set things up"

[Ruben Van de Velde]

I think it's worth having, but probably also to have iffs for each with the preferred spelling (which is probably AlexandrovDiscrete X)

[Eric Wieser]

But only put the things in it that actually help, the goal is not to try and make the tfae exhaustive, as that's what the API is for

[Aaron Liu]

Eric Wieser said:

But only put the things in it that actually help, the goal is not to try and make the tfae exhaustive, as that's what the API is for

How do I know what helps?

[Yakov Pechersky]

Make the TFAE be 1 → 15 → 8 → 14 → 17 → 2 ↔ 1, expose 15 ↔ 1, 8 ↔ 1, 14 ↔ 1, 17 ↔ 1, 2 ↔ 1 as separate lemmas, use those separate lemmas for the remainder of the statements you have in your list.

[Aaron Liu]

ok let me collect all my tfae lemmas here so you can see why I don't know which ones are "necessary"

• 1 ↔ 2
• 8 → 9
• 1 → 15
• 1 → 11
• 1 → 12
• 1 → 3
• 9 ↔ 10
• 9 → 2
• 7 → 6
• 2 → 7
• 3 → 2
• 6 → 5
• 17 → 2
• 16 → 17
• 17 → 16
• 15 → 8
• 11 → 2
• 12 → 11
• 4 → 5
• 5 → 2
• 2 → 4
• 8 → 14
• 13 ↔ 14
• 14 → 17

[Bolton Bailey]

Screenshot 2025-05-02 at 10.43.07 AM.png Here is a flowchart if that helps

[Aaron Liu]

Bolton Bailey said:

Screenshot 2025-05-02 at 10.43.07 AM.png

neat

[Aaron Liu]

so to me it's still not very clear which ones are the main results

[Aaron Liu]

and it looks like I can delete 1 → 2 and 1 → 11, making my proof 1 line shorter (it's 200 lines long)

[Eric Wieser]

I'd perhaps suggest making the 1,2,3 loop (since 1 is the canonical spelling) with TFAE, then adding the two API lemmas, then doing a TFAE for the remainder of the graph with those edged contracted.

[Eric Wieser]

10, 13, and 16 could be dropped from it entirely

[Aaron Liu]

I'm thinking I'll just put the tfae in and then add a bunch of alexandrovDiscrete_iff_foo lemmas right after

[Andrew Yang]

I claim that TFAEs, while hard to apply and should definitely have the iff lemmas succeeding it, is a nice way to present the results and is good for discoverability and thus should be kept.

[Aaron Liu]

btw, where should this go? In file#Topology/AlexandrovDiscrete, or in a new file?

[Eric Wieser]

If some of the proofs need more machinery than others, this might be good evidence not to put everything in a TFAE

[Eric Wieser]

Andrew Yang said:

I claim that TFAEs, while hard to apply and should definitely have the iff lemmas succeeding it, is a nice way to present the results and is good for discoverability and thus should be kept.

I'd argue the discoverability mechanism here is @loogle AlexandrovDiscrete _ \iff _

[Aaron Liu]

The problem is that Topology.upperSet, used in the statement, is defined in a later file.

[Eric Wieser]

Then you should definitely prove the 1-2-3 loop separately, in an earlier file

[Andrew Yang]

I don't think it is reasonable to assume that an external tool which requires internet access and requests to online servers should be the main discoverability mechanism.

[Eric Wieser]

Loogle can be used offline, just like the docs can

[Eric Wieser]

And frankly a grep would be equally effective here

[Eric Wieser]

(which is also what you'd do to find the TFAE, but there the grep is more complicated)

[Andrew Yang]

But a bunch of iffs scattered in different places each perhaps with different side conditions that you need to check one by one is less straightforward to users (at least to me) compared to say two big lists of tfaes where one has one side condition and one has the other.

[Andrew Yang]

Eric Wieser said:

Loogle can be used offline, just like the docs can

And (perhaps off topic but) how do I do this?

[Eric Wieser]

I think the reality of mathlib is that it's not wise or even possible to put all the Iffs that you could possibly care about in once place

[Eric Wieser]

(I suggest a new thread for the loogle question)

[Andrew Yang]

Eric Wieser said:

I think the reality of mathlib is that it's not wise or even possible to put all the Iffs that you could possibly care about in once place

So this is why you put a tfae at the end to point to all the iff lemmas proved somewhere in the library.

[Yaël Dillies]

But then the file this TFAE lives in is unimportable, since all its constituent parts have fewer dependencies

[Eric Wieser]

"at the end" here has to mean "at the end of the import (sub)graph" not "at the end of the file"

[Eric Wieser]

At which point, what makes it discoverable?

[Andrew Yang]

As in you don't need to remember all the iff lemmas scattered around the library and you can just remember one declaration and consult that when necessary.

[Aaron Liu]

So what should I do with this proof?

[Eric Wieser]

My vote would be split it

[Jireh Loreaux]

@Thomas Murrills not sure if that extension is still on your radar, but if so, this seems like a good test case.

[Aaron Liu]

Eric Wieser said:

My vote would be split it

What should I split it into?

[Thomas Murrills]

Jireh Loreaux said:

Thomas Murrills not sure if that extension is still on your radar, but if so, this seems like a good test case.

I haven’t worked on it lately, but it still is on my radar! I’ve been lurking in this thread and thinking the same thing… :grinning_face_with_smiling_eyes:

[Eric Wieser]

Aaron Liu said:

Eric Wieser said:

My vote would be split it

What should I split it into?

Put the 1-2-3 cycle (and anything else that fits) into the existing file, and everything else into a new file with heavier imports.