The Following Are Equivalent #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file allows to state that all propositions in a list are equivalent. It is used by
tfae l means
∀ x ∈ l, ∀ y ∈ l, x ↔ y. This is equivalent to
pairwise (↔) l.
tfae: The Following (propositions) Are Equivalent.
tfae_finish tactics can be useful in proofs with
- l.tfae = ∀ (x : Prop), x ∈ l → ∀ (y : Prop), y ∈ l → (x ↔ y)