Zulip Chat Archive

Stream: new members

Topic: What is the correct/preferred way to TFAE

kvanvels (Aug 15 2022 at 23:09):

I am trying to express a theorem that is structure like : The following are three propositions are equivalent:
1) proposition A
2) proposition B
3) proposition C

My proof will most likely be A \to B, B \to C, and C \to A.
What is a the preferred/correct way to write this up? Is there any example in mathlib or elsewhere that uses this kind of proof/theorem?

I appreciate any direction. I am using lean4 but lean3 ideas will be very much appreciated.

Junyan Xu (Aug 15 2022 at 23:10):


Adam Topaz (Aug 15 2022 at 23:11):

And to use it we have docs#list.tfae.out

kvanvels (Aug 15 2022 at 23:12):

Thanks, this community is great. Thank you. I will follow up if I have more questions.

Adam Topaz (Aug 15 2022 at 23:12):

I would also look at the tactic list and search for tfae

Adam Topaz (Aug 15 2022 at 23:12):

We have some nice helper tactics for proving such statements

Junyan Xu (Aug 15 2022 at 23:12):

Notice that docs#tactic.interactive.tfae_have use 1-based indexing but docs#list.tfae.out is 0-based, if I recall correctly.

Adam Topaz (Aug 15 2022 at 23:13):

yeah, this inconsistency is annoying

Eric Wieser (Aug 15 2022 at 23:13):

Note that often what actually happens is that we choose A as the canonical definition and call it my_prop, then write the lemmas my_prop <-> A (by definition), my_prop <-> B, my_prop <-> C

Eric Wieser (Aug 15 2022 at 23:14):

In my experience, tfae is nice for transcribing a pen and paper result, but not all that convenient for building things on top of.

Adam Topaz (Aug 15 2022 at 23:14):

It's nice when you have more than 3 statements

Eric Wieser (Aug 15 2022 at 23:15):

I guess for the case I describe you might use tfae under the hood to build the API

Adam Topaz (Aug 15 2022 at 23:15):

Or some giant connected digraph of implications and you don't want to manually construct a path between two nodes

Last updated: Dec 20 2023 at 11:08 UTC