List.exists_tfae
theorem List.exists_tfae :
∀ {α : Type u_1} (l : List (α → Prop)),
(∀ (a : α), (List.map (fun p => p a) l).TFAE) → (List.map (fun p => ∃ a, p a) l).TFAE
The theorem `List.exists_tfae` in Lean 4 states that for a list of predicates `l` over a certain type `α`, if for every element `a` of type `α` the predicates in the list are equivalent (i.e., `(P₁ a) ↔ (P₂ a) ↔ ... ↔ (Pₙ a)`), then the existential statements of these predicates are also equivalent (i.e., `(∃ a, P₁ a) ↔ (∃ a, P₂ a) ↔ ... ↔ (∃ a, Pₙ a)`). The theorem can be applied in concrete cases where Lean 4 has trouble finding the list of predicates from the list of existential statements, by providing a list of placeholders with the appropriate length.
More concisely: If for all elements `a` of type `α`, the predicates `P₁, P₂, ..., Pₙ` are equivalent, then the existential statements `∃ a, P₁ a`, `∃ a, P₂ a`, ..., `∃ a, Pₙ a` are equivalent.
|
List.TFAE.out
theorem List.TFAE.out :
∀ {l : List Prop},
l.TFAE →
∀ (n₁ n₂ : ℕ) {a b : Prop},
autoParam (l.get? n₁ = some a) _auto✝ → autoParam (l.get? n₂ = some b) _auto✝¹ → (a ↔ b)
The theorem `List.TFAE.out` states that if a list of propositions (`l`) is such that all propositions are equivalent to each other (expressed by `List.TFAE l`), then for any two indices `n₁` and `n₂`, and two propositions `a` and `b`, if `a` and `b` are the propositions at index `n₁` and `n₂` in the list respectively (expressed by `List.get? l n₁ = some a` and `List.get? l n₂ = some b`), then `a` and `b` are equivalent. The `autoParam` function is used to automatically provide these last two conditions when they are not explicitly provided. The proof of this theorem is not shown here as it is represented by `sorry`.
More concisely: If a list `l` of propositions satisfies `List.TFAE l`, then for any indices `n₁` and `n₂`, the propositions at indices `n₁` and `n₂` are equivalent, i.e., `List.get? l n₁ ≈ List.get? l n₂`.
|
List.tfae_of_cycle
theorem List.tfae_of_cycle :
∀ {a b : Prop} {l : List Prop},
List.Chain (fun x x_1 => x → x_1) a (b :: l) → (l.getLastD b → a) → (a :: b :: l).TFAE
The theorem `List.tfae_of_cycle` states that for any two propositions `a` and `b`, and a list of propositions `l`, if `a` logically implies each proposition in the list `b :: l` in sequence (`List.Chain`), and the last proposition in the list `l` with a default of `b` (`List.getLastD l b`) implies `a`, then all propositions in the list `a :: b :: l` are logically equivalent (`List.TFAE`). In other words, this theorem provides a way to show that a cyclic chain of implications among a list of propositions implies the logical equivalence of these propositions.
More concisely: If `a` implies every `b : l` and the last `b` (or `a` if `l` is empty) implies `a`, then `a` is logically equivalent to each `b` in the list `a :: b :: l`.
|
List.forall_tfae
theorem List.forall_tfae :
∀ {α : Type u_1} (l : List (α → Prop)),
(∀ (a : α), (List.map (fun p => p a) l).TFAE) → (List.map (fun p => ∀ (a : α), p a) l).TFAE
This theorem states that if for any element `x` from a type `α`, the properties `P₁ x, ..., Pₙ x` are all logically equivalent (i.e., `P₁ x ↔ ... ↔ Pₙ x`), then the assertions that these properties hold for all `x` are also logically equivalent, i.e., `(∀ x, P₁ x) ↔ ... ↔ (∀ x, Pₙ x)`.
In more detail, given a list `l` of properties about elements of type `α`, if for each `a` of type `α`, applying the properties to `a` results in a list of truth values that are all equivalent (The acronym 'TFAE' stands for 'The Following Are Equivalent'), then a new list of universal statements, formed by saying that each property holds for all `a`, also has the property that all its entries are equivalent. The theorem also notes that in practical usage, Lean may have difficulty inferring the list of properties from the list of universal statements, but providing a list of underscores with the correct length can help it to infer correctly.
More concisely: If a list of properties `P₁, ..., Pₙ` is such that `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∀ x, P₁ x) ↔ ... ↔ (∀ x, Pₙ x)` holds logically. (This is known as the "Theorem of the Uniformly Equivalent Families" or "TFAE theorem" in Lean logic.)
|