usize_size_eq
theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616
This theorem states that the size of the unsigned size (USize) in Lean is either 4294967296 or 18446744073709551616. This is equivalent to saying that the size of USize is either 32 bits or 64 bits, depending on the system architecture.
More concisely: The size of Lean's unsigned integer type USize is either 32 or 64 bits, equivalent to having a range of 2^32 or 2^64 possible values.
|
System.Platform.numBits_eq
theorem System.Platform.numBits_eq : System.Platform.numBits = 32 ∨ System.Platform.numBits = 64
The theorem `System.Platform.numBits_eq` states that the word size of the current platform, as defined by `System.Platform.numBits`, is either 32 or 64. That is, it asserts that the platform is either a 32-bit or a 64-bit system.
More concisely: The theorem `System.Platform.numBits_eq` asserts that `System.Platform.numBits` is equal to either 32 or 64.
|
ULift.down_up
theorem ULift.down_up : ∀ {α : Type u} (a : α), { down := a }.down = a
This theorem states that for any type `α` and any element `a` of this type, constructing a `ULift` object with `a` as the `down` field and then accessing the `down` field of this object yields the original value `a`. In other words, the operations of lifting a value into the `ULift` type and then retrieving it are inverses of each other. The `ULift` type is essentially a wrapper around the original type `α`, allowing us to manipulate `α` values at a different universe level `v`.
More concisely: For any type `α` and its element `a`, the operation of lifting `a` to `ULift α` and then taking its `down` field gives the original `a`. In symbols, `down (ULift.lift α a) = a`.
|
Nat.le_of_lt_succ
theorem Nat.le_of_lt_succ : ∀ {m n : ℕ}, m < n.succ → m ≤ n
This theorem states that for any two natural numbers `m` and `n`, if `m` is less than the successor of `n` (in other words, `m` is less than `n+1`), then `m` is less than or equal to `n`. It essentially formalizes the intuitive fact that if a number is less than the next number after another, it must be less than or equal to that other number.
More concisely: If `m` is less than `n+1`, then `m` is less than or equal to `n`.
|
of_decide_eq_false
theorem of_decide_eq_false : ∀ {p : Prop} [inst : Decidable p], decide p = false → ¬p
This theorem states that for any proposition `p` that has a decidable truth value, if the decision procedure `decide p` for `p` returns false, then the proposition `p` is not true. In other words, it confirms that the `decide` function correctly identifies propositions that are false within the context of classical logic.
More concisely: If `decide p` returns false for a proposition `p` in classical logic, then `p` is false.
|
Nat.lt_of_le_of_lt
theorem Nat.lt_of_le_of_lt : ∀ {n m k : ℕ}, n ≤ m → m < k → n < k
This theorem states that for any three natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m` and `m` is strictly less than `k`, then `n` is strictly less than `k`. In mathematical terms, it defines a property of the ordering of natural numbers, specifically: if \(n \leq m\) and \(m < k\), then \(n < k\).
More concisely: If \(n \leq m\) and \(m < k\), then \(n < k\).
|
eq_of_heq
theorem eq_of_heq : ∀ {α : Sort u} {a a' : α}, HEq a a' → a = a'
This theorem, `eq_of_heq`, states that for any type `α` and any two elements `a` and `a'` of type `α`, if `a` is heterogeneously equal to `a'` (denoted as `HEq a a'`), then `a` is also homogeneously equal to `a'` (denoted as `a = a'`). In other words, if two elements are equivalent in a type-independent manner (`HEq`), they are also equivalent in a type-dependent manner (`=`).
More concisely: If `α` is a type and `a` and `a'` are elements of `α` with `HEq a a'`, then `a = a'`.
|
of_decide_eq_true
theorem of_decide_eq_true : ∀ {p : Prop} [inst : Decidable p], decide p = true → p
This theorem, `of_decide_eq_true`, states that for any proposition `p`, given that `p` is decidable (meaning it can be determined whether `p` is true or false), if the decision procedure for `p` returns `true`, then `p` is indeed true. Essentially, it asserts the correctness of the decision procedure: if `decide p` is `true`, then `p` holds.
More concisely: If a proposition `p` is decidable and its decision procedure returns `true`, then `p` is true.
|
Nat.succ_le_succ
theorem Nat.succ_le_succ : ∀ {n m : ℕ}, n ≤ m → n.succ ≤ m.succ
This theorem, `Nat.succ_le_succ`, states that for all natural numbers `n` and `m`, if `n` is less than or equal to `m`, then the successor of `n` (i.e. `n + 1` in mathematics, represented as `Nat.succ n` in Lean 4) is less than or equal to the successor of `m` (i.e. `m + 1` in mathematics, represented as `Nat.succ m` in Lean 4). This theorem essentially captures the intuitive notion that increasing both sides of an inequality by the same amount preserves the inequality.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m` then `Nat.succ n ≤ Nat.succ m`.
|
Or.resolve_right
theorem Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a
This theorem, named "Or.resolve_right", states that for any two propositions `a` and `b`, if `a` OR `b` is true and `b` is not true (denoted as ¬b), then `a` must be true. Essentially, it resolves a disjunction from the right, eliminating the possibility of the right-hand proposition being true, and concluding that the left-hand proposition has to be true.
More concisely: If `a` OR `b` is true and `b` is false, then `a` is true.
|
Nat.zero_lt_succ
theorem Nat.zero_lt_succ : ∀ (n : ℕ), 0 < n.succ
This theorem states that for every natural number `n`, the successor of `n` is always greater than zero. In other words, it's saying that if you add 1 to any natural number, the result will always be greater than zero. This is a basic property of natural numbers in the system of Peano axioms, which is the basis for the standard theory of natural numbers in mathematics.
More concisely: For every natural number `n`, `n + 1` is positive. (Or, equivalently, `0 < Suc n`, where `Suc` is the successor function.)
|
Nat.le_of_ble_eq_true
theorem Nat.le_of_ble_eq_true : ∀ {n m : ℕ}, n.ble m = true → n ≤ m
This theorem states that for all natural numbers `n` and `m`, if the function `Nat.ble n m` returns `true`, then `n` is less than or equal to `m`. The function `Nat.ble` checks if `n` is less than or equal to `m` using Boolean logic, returning a Boolean value. Therefore, this theorem connects the Boolean logic of `Nat.ble` with the mathematical property of less than or equal to (`≤`).
More concisely: For all natural numbers n and m, if Nat.ble n m holds, then n ≤ m.
|
And.left
theorem And.left : ∀ {a b : Prop}, a ∧ b → a
The theorem `And.left` states that for any two propositions `a` and `b`, if there exists a proof of the conjunction `a ∧ b`, then there exists a proof of `a`. In other words, if `a` and `b` are both true, then `a` is true. This theorem is useful for extracting the left part of a conjunction. This operation can be denoted as `h.left` or `h.1`, where `h` is the proof of `a ∧ b`.
More concisely: If `a ∧ b` is provable, then `a` is provable.
|
Or.intro_right
theorem Or.intro_right : ∀ {b : Prop} (a : Prop), b → a ∨ b
This theorem, `Or.intro_right`, is an alias for `Or.inr` in Lean. Given two propositional variables, a and b, it states that if we have a proof of b, then we can establish the proof of the logical disjunction "a OR b". Note that there isn't any necessity for a to be true for this theorem.
More concisely: If we have a proof of proposition b, then we can derive a proof of the logical disjunction a OR b in Lean.
|
ULift.up_down
theorem ULift.up_down : ∀ {α : Type u} (b : ULift.{v, u} α), { down := b.down } = b
This theorem states that for any type `α` and any term `b` of the type `ULift.{v, u} α`, creating a new `ULift` term by extracting the `down` value of `b` and using it as the new `down` value results in `b` itself. In other words, it states that there is a bijection between `α` and `ULift.{v} α`. This is similar to saying that you can "lift" a value into the `ULift` type and then "bring it down" again without changing the value.
More concisely: For any type `α` and `ULift.{v} α` term `b`, `ULift.down (ULift.lift down b)` equals `b`.
|
Nat.pred_le_pred
theorem Nat.pred_le_pred : ∀ {n m : ℕ}, n ≤ m → n.pred ≤ m.pred
The theorem `Nat.pred_le_pred` states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m` (expressed as `n ≤ m`), then the predecessor of `n` is also less than or equal to the predecessor of `m` (expressed as `Nat.pred n ≤ Nat.pred m`). Here, the predecessor of a natural number `x` is defined as `x - 1` if `x` is not zero, and it remains zero if `x` is zero.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m` then `Nat.pred n ≤ Nat.pred m`.
|
Nat.not_succ_le_zero
theorem Nat.not_succ_le_zero : ∀ (n : ℕ), n.succ ≤ 0 → False
This theorem asserts that for any natural number `n`, the successor of `n` cannot be less than or equal to zero. In other words, if you have any natural number and add one to it, the result is never less than or equal to zero. This makes sense since natural numbers start from zero and increase; thus, their successors are always greater than zero.
More concisely: For all natural numbers n, the successor of n is strictly greater than zero.
|
List.get.proof_2
theorem List.get.proof_2 :
∀ {α : Type u_1} (head : α) (as : List α) (i : ℕ), i.succ < (head :: as).length → i.succ ≤ as.length
This theorem states that for any type `α`, any list of `α` named `as`, any element of `α` named `head`, and any natural number `i`, if `i+1` is less than the length of the list created by prepending `head` to `as`, then `i+1` is less than or equal to the length of the list `as`. Roughly speaking, this says that if some index `i+1` is a valid index for a list `head :: as`, then `i+1` will also be a valid index or just one more than the length of the list `as`.
More concisely: For any list `as : α :: list α` and natural number `i`, if `length (cons α as) > i + 1`, then `length as <= i + 1`.
|
id_eq
theorem id_eq : ∀ {α : Sort u_1} (a : α), id a = a
This theorem states that for any given type `α` and any element `a` of that type, the identity function `id` applied to `a` is equal to `a` itself. It's marked as a simplification lemma, meaning that Lean will automatically apply it to simplify expressions during proof search.
More concisely: For any type `α` and its element `a`, the identity function `id a = a`.
|
Or.resolve_left
theorem Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b
This theorem, `Or.resolve_left`, states that for any two propositions `a` and `b`, if the disjunction of `a` and `b` (`a ∨ b`) is true and the negation of `a` (`¬a`) is also true, then `b` must be true. In other words, if `a` or `b` is true and we know that `a` is not true, then `b` has to be true. This is a fundamental rule in logic, often used in logical reasoning and proofs.
More concisely: If `a ∨ b` is true and `¬a` is true, then `b` is true.
|
Subtype.property
theorem Subtype.property : ∀ {α : Sort u} {p : α → Prop} (self : Subtype p), p ↑self
This theorem states that for any subtype `s`, which is defined as a set of elements `x` for which a property `p` holds, `s.2` or `s.property` asserts that the property `p` holds for `s.1`, i.e. the underlying element of `s`. In other words, `s` is indeed an element for which property `p` is true.
More concisely: For any subtype `s` in Lean 4, `s.property` holds for the underlying element `s.1`.
|
Or.intro_left
theorem Or.intro_left : ∀ {a : Prop} (b : Prop), a → a ∨ b
This theorem, named `Or.intro_left`, is an alias for `Or.inl` and is used to introduce the "or" logical operator (`∨`). It states that for any two propositions `a` and `b`, if `a` is true, then the proposition " `a ∨ b` " is also true. In other words, it's a way to confirm that if you have a proof of `a`, you can use that to create a proof of `a ∨ b`, regardless of whether `b` is true or not.
More concisely: If `a` is a proposition, then `a ∨ b` holds. (Assumes `b` is arbitrary.)
|
Nat.lt_of_le_of_ne
theorem Nat.lt_of_le_of_ne : ∀ {n m : ℕ}, n ≤ m → ¬n = m → n < m
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m` and `n` is not equal to `m`, then `n` is less than `m`. In other words, it confirms the property that when two natural numbers are not equal, and one is not greater than the other, then it must be strictly less than the other.
More concisely: For all natural numbers `n` and `m`, if `n` < `m` and `n` ≠ `m`, then `n` < `m`.
|
And.right
theorem And.right : ∀ {a b : Prop}, a ∧ b → b
This theorem is about extracting the right element from a proposition that is a conjunction. Given a conjunction `a ∧ b`, denoted as `h`, the theorem states that `h.right` or `h.2` is a proof of `b`. In other words, if you have a proposition that `a` and `b` are both true, then you can directly assert the truth of `b`.
More concisely: Given a conjunction `h : p ∧ q`, the right component `h.2` is a proof of `q`.
|
Nat.le_succ_of_le
theorem Nat.le_succ_of_le : ∀ {n m : ℕ}, n ≤ m → n ≤ m.succ
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then `n` is also less than or equal to the successor of `m` (i.e., `m+1`). This essentially captures the intuitive notion that if a number is less than or equal to another number, it will also be less than or equal to any number greater than that number.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m`, then `n ≤ m + 1`.
|
Fin.eq_of_val_eq
theorem Fin.eq_of_val_eq : ∀ {n : ℕ} {i j : Fin n}, ↑i = ↑j → i = j
This theorem states that for any natural number `n` and for any two elements `i` and `j` of the finite set `Fin n`, if the numerical values of `i` and `j` are equal (denoted by ↑i = ↑j), then `i` and `j` themselves are equal. Essentially, it asserts that distinct elements of a finite set `Fin n` must have distinct numerical values.
More concisely: For any finite set `Fin n` and all `i`, `j` in `Fin n`, if `i` and `j` have equal numerical values, then `i` and `j` are equal.
|
Eq.subst
theorem Eq.subst : ∀ {α : Sort u} {motive : α → Prop} {a b : α}, a = b → motive a → motive b
This theorem, known as the substitution principle for equality, states that, given any type `α`, a predicate `motive` that applies to `α`, and two objects `a` and `b` of type `α`, if `a` equals `b` and the `motive` holds true for `a`, then the `motive` also holds true for `b`. Essentially, this means that if `a` and `b` are equal, anything that is true about `a` is also true about `b`. This principle is fundamental to the `rw` (rewrite) tactic in Lean, which uses this theorem to replace occurrences of `a` with `b` in a mathematical expression or proof goal.
More concisely: If `a = b` and `P(a)` holds, then `P(b)` holds. (The statement `P(a)` is a predicate `motive` that applies to type `α` in Lean.)
|
Nat.le_of_succ_le_succ
theorem Nat.le_of_succ_le_succ : ∀ {n m : ℕ}, n.succ ≤ m.succ → n ≤ m
This theorem states that for any two natural numbers `n` and `m`, if the successor of `n` (i.e., `n + 1`) is less than or equal to the successor of `m` (i.e., `m + 1`), then `n` is less than or equal to `m`. It essentially allows us to remove a "successor" operation from both sides of an inequality.
More concisely: If `n + 1 ≤ m + 1`, then `n ≤ m`.
|
decide_eq_false
theorem decide_eq_false : ∀ {p : Prop} [inst : Decidable p], ¬p → decide p = false
This theorem, `decide_eq_false`, is stating that for any proposition `p`, given that `p` is decidable (meaning we have an instance of `Decidable p`), if `¬p` (i.e., `p` is not true), then the function `decide p` will return `false`. In simple words, if some proposition is not true, then its decision function will confirm this by returning `false`. This theorem can be used in the context of constructive logic, where we need explicit proof or disproof (decision procedures) for our propositions.
More concisely: If `p` is a decidable proposition in Lean 4 and `¬p` holds, then `decide p` returns `false`.
|
PLift.down_up
theorem PLift.down_up : ∀ {α : Sort u} (a : α), { down := a }.down = a
This theorem states that for any type `α` and any element `a` of this type, if we construct a `PLift` structure `{ down := a }` and then extract its `down` field, we get the original element `a` back. In other words, the functions that create a `PLift` and extract its `down` field constitute a bijection between `α` and `PLift α`, thus preserving the identity of its elements.
More concisely: The `PLift` construction and extraction of the `down` field define a bidirectional bijection between any type `α` and its associated `PLift α` type.
|
decide_eq_true
theorem decide_eq_true : ∀ {p : Prop} [inst : Decidable p], p → decide p = true
This theorem, named `decide_eq_true`, establishes that for any proposition `p` of type `Prop` and given that `p` is decidable (i.e., there exists a proof or disproof for `p`), if `p` is true, then the function `decide` applied to `p` is equal to `true`. Essentially, it states that if a proposition is true and decidable, applying the decision function to that proposition will return `true`.
More concisely: If `p` is a decidable proposition of type `Prop` in Lean 4 and `p` is true, then `decide p = true`.
|
Nat.not_succ_le_self
theorem Nat.not_succ_le_self : ∀ (n : ℕ), ¬n.succ ≤ n
This theorem states that for any natural number `n`, the successor of `n` (which can be thought of as `n + 1`) is not less than or equal to `n`. In other words, the assertion is that no natural number is greater than or equal to its immediate successor, which aligns with our standard understanding of natural numbers in mathematics.
More concisely: For all natural numbers n, n < succ(n).
|
Nat.le_refl
theorem Nat.le_refl : ∀ (n : ℕ), n ≤ n
This theorem, `Nat.le_refl`, is an assertion about the reflexivity of less than or equal to relation on natural numbers. It states that for any natural number `n`, `n` is less than or equal to itself. In other words, it proves the property of reflexivity for the "less than or equal to" relation in the set of natural numbers.
More concisely: For all natural numbers n, n ≤ n.
|
Nat.lt_trans
theorem Nat.lt_trans : ∀ {n m k : ℕ}, n < m → m < k → n < k
This theorem, `Nat.lt_trans`, is a statement about the transitivity of the 'less than' relation on natural numbers. Specifically, it asserts that for any three natural numbers `n`, `m`, and `k`, if `n` is less than `m` and `m` is less than `k`, then `n` is less than `k`. In mathematical notation, this would be expressed as: ∀ {n m k : ℕ}, n < m → m < k → n < k. This is a fundamental property of ordered sets.
More concisely: For all natural numbers `n, m, k`, if `n` is less than `m` and `m` is less than `k`, then `n` is less than `k` (i.e., `n < m` and `m < k` imply `n < k`).
|
Nat.le_succ
theorem Nat.le_succ : ∀ (n : ℕ), n ≤ n.succ
This theorem states that for any natural number `n`, `n` is less than or equal to its successor (`n + 1`). That means, in any situation where you have a natural number, it will always be less than or equal to the next natural number.
More concisely: For all natural numbers n, n ≤ n+1.
|
congr
theorem congr : ∀ {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α}, f₁ = f₂ → a₁ = a₂ → f₁ a₁ = f₂ a₂
The `congr` theorem states that given two sets of nondependent functions and their respective arguments (`f₁`, `a₁`) and (`f₂`, `a₂`), if the functions (`f₁` and `f₂`) are equal and the arguments (`a₁` and `a₂`) are also equal, then applying the function to the argument (`f₁ a₁` and `f₂ a₂`) will also yield equal results. This theorem is applicable in the field of mathematical logic and functional programming where function and argument congruence is necessary. Note that the theorem becomes more complex in the case of dependent functions.
More concisely: If functions `f₁` and `f₂` are equal and their arguments `a₁` and `a₂` are equal, then `f₁ a₁` and `f₂ a₂` are equal.
|
Nat.lt_irrefl
theorem Nat.lt_irrefl : ∀ (n : ℕ), ¬n < n
This theorem, `Nat.lt_irrefl`, states that for all natural numbers `n`, `n` is not less than `n`. In other words, no natural number is less than itself.
More concisely: For all natural numbers n, n ≤ n is false.
|
PLift.up_down
theorem PLift.up_down : ∀ {α : Sort u} (b : PLift α), { down := b.down } = b
This theorem states that there is a bijection between any type `α` and the `PLift` of `α`. In other words, for any 'lifted' value `b` of the type `PLift α`, recreating a `PLift` object from the 'down' value of `b` (which is of type `α`) gives us back the original 'lifted' value `b`. This demonstrates that the process of lifting a type with `PLift` and then taking it back down with 'down' is fully reversible.
More concisely: The function from `α` to `PLift α` given by lifting, and the function from `PLift α` to `α` given by downcasting, form a bijection.
|
Nat.lt_or_ge
theorem Nat.lt_or_ge : ∀ (n m : ℕ), n < m ∨ n ≥ m
This theorem, `Nat.lt_or_ge`, states that for any two natural numbers `n` and `m`, either `n` is less than `m`, or `n` is greater than or equal to `m`. In other words, given any two natural numbers, one is always either smaller than or at least as large as the other. This relationship is a fundamental property of the natural numbers.
More concisely: For all natural numbers n and m, either n < m or n >= m.
|
Nat.le_trans
theorem Nat.le_trans : ∀ {n m k : ℕ}, n ≤ m → m ≤ k → n ≤ k
This theorem, `Nat.le_trans`, is a statement about the transitivity of the "less than or equal to" relation in the context of natural numbers. It states that for any three natural numbers `n`, `m`, and `k`, if `n` is less than or equal to `m` and `m` is less than or equal to `k`, then `n` is less than or equal to `k`. This is a fundamental property of order relations.
More concisely: If `n` is less than or equal to `m` and `m` is less than or equal to `k`, then `n` is less than or equal to `k` (`n ≤ m` and `m ≤ k` imply `n ≤ k`).
|
Nat.zero_le
theorem Nat.zero_le : ∀ (n : ℕ), 0 ≤ n
This theorem states that for any natural number 'n', 0 is less than or equal to 'n'. In other words, zero is always less than or equal to any given natural number. This is a fundamental property of natural numbers in mathematics, as no natural number can be negative.
More concisely: For all natural numbers n, 0 ≤ n.
|
Nat.le_antisymm
theorem Nat.le_antisymm : ∀ {n m : ℕ}, n ≤ m → m ≤ n → n = m
This theorem is named `Nat.le_antisymm` and it states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m` and `m` is less than or equal to `n`, then `n` must be equal to `m`. In other words, this is the antisymmetry property of the less than or equal to relation on natural numbers: it cannot be the case that both `n ≤ m` and `m < n` for natural numbers `n` and `m`.
More concisely: If `n` is less than or equal to `m` and `m` is less than or equal to `n` then `n` equals `m`. (Antisymmetry property of the less-than-or-equal relation on natural numbers)
|
congrArg
theorem congrArg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
The theorem `congrArg` states that for any types `α` and `β`, given two elements `a₁` and `a₂` of type `α`, and any function `f` from `α` to `β`, if `a₁` equals `a₂` then the function `f` applied to `a₁` equals the function `f` applied to `a₂`. In other words, this theorem asserts that a function applied to equal arguments produces equal results. This is not just applicable to functions but also to lambda expressions. This theorem is frequently used by tactics such as `congr` and `simp` in Lean to apply equalities within subterms.
More concisely: For all types α and β, and for all functions f from α to β and elements a₁ and a₂ of type α, if a₁ = a₂ then f(a₁) = f(a₂).
|
Eq.symm
theorem Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a
This theorem states that equality is symmetric, meaning if `a` equals `b`, then `b` equals `a`. Here, `α` denotes any type or sort, and `a` and `b` are variables of this type. If you have a proof `h` that `a = b`, you can use `h.symm` or `Eq.symm h` to obtain a proof of `b = a`. This theorem is a fundamental property of equality in logic and mathematics.
More concisely: If `a = b`, then `b = a`. (Equality is reflexive and symmetric.)
|
Eq.trans
theorem Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c
This theorem states that equality is transitive in Lean 4. In other words, if you have two equalities, `a = b` and `b = c`, (represented as `h₁ : a = b` and `h₂ : b = c`), you can use the transitivity of equality to infer that `a = c`. This can be done using the shorthand `h₁.trans h₂ : a = c` or the longer form `Eq.trans h₁ h₂`. This theorem is applicable for any sort `α` and variables `a`, `b`, and `c` of sort `α`.
More concisely: If `a = b` and `b = c`, then `a = c` (transitivity of equality).
|
Nat.not_lt_zero
theorem Nat.not_lt_zero : ∀ (n : ℕ), ¬n < 0
This theorem states that for all natural numbers `n`, `n` is not less than zero. In other words, it's impossible for any natural number to be less than zero. This is intuitive, as the set of natural numbers starts from zero and includes all positive integers.
More concisely: The theorem asserts that for all natural numbers `n`, `0 ≤ n`.
|
Nat.ble_eq_true_of_le
theorem Nat.ble_eq_true_of_le : ∀ {n m : ℕ}, n ≤ m → n.ble m = true
This theorem states that for every pair of natural numbers `n` and `m`, if `n` is less than or equal to `m`, then the result of the function `Nat.ble n m` (which checks if `n` is less than or equal to `m` and returns a boolean) is `true`. Essentially, this theorem formalizes part of the definition of the "less than or equal to" relation for natural numbers in terms of a boolean function.
More concisely: For all natural numbers `n` and `m`, `Nat.ble n m` holds if and only if `n` is less than or equal to `m`.
|
Or.elim
theorem Or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
This theorem, `Or.elim`, is a proof by cases on an `Or` proposition. It states that, given three propositions `a`, `b`, and `c`, if the disjunction `a ∨ b` is true, and if both `a` and `b` imply `c` (i.e., `a → c` and `b → c`), then `c` must also be true. Essentially, it allows you to conclude `c` if you know that either `a` or `b` is true, and either one would imply `c`.
More concisely: If `a ∨ b` holds and `a → c` and `b → c` are true in Lean 4 logic, then `c` is also true.
|
List.length_cons
theorem List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α), (a :: as).length = as.length.succ
The theorem `List.length_cons` asserts that for any type `α`, any element `a` of type `α`, and any list `as` of elements of type `α`, the length of the list formed by consing `a` onto `as` (denoted `a :: as`) is equal to the successor (`Nat.succ`) of the length of `as`. In other words, adding an element to the front of a list increases the length of the list by one.
More concisely: For any type `α` and lists `a :: as` of elements of type `α`, the length of the list `a :: as` is the successor of the length of `as`. In Lean syntax, `(List.length (a :: as)) = Nat.succ (List.length as)`.
|
Fin.isLt
theorem Fin.isLt : ∀ {n : ℕ} (self : Fin n), ↑self < n
This theorem states that for any given `n` of type natural number `ℕ` and any `i` of type `Fin n` (finite set of natural numbers less than `n`), the value `↑i` (which is the actual number represented by `i`) is strictly less than `n`. In other words, this theorem validates the definition of `Fin n` as a set of natural numbers less than `n`.
More concisely: For all natural numbers `n` and `i` in `Fin n`, the value `i` represents a number strictly less than `n`.
|
Nat.eq_or_lt_of_le
theorem Nat.eq_or_lt_of_le : ∀ {n m : ℕ}, n ≤ m → n = m ∨ n < m
This theorem states that for any two natural numbers `n` and `m`, if `n` is less than or equal to `m`, then either `n` is equal to `m` or `n` is less than `m`. In other words, if `n` is not greater than `m`, it must be either equal or strictly less. This is a basic property of the ordering of natural numbers and is similar to the trichotomy property.
More concisely: For all natural numbers `n` and `m`, if `n ≤ m`, then `n = m` or `n < m`.
|
Or.neg_resolve_left
theorem Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b
This theorem, `Or.neg_resolve_left`, states that for any two propositions `a` and `b`, if the disjunction of the negation of `a` and `b` is true, and `a` is also true, then `b` must be true. In mathematical terms, for all propositions `a` and `b`, `(¬a ∨ b) → a → b`. This means if either `a` is not true or `b` is true, and if `a` is true, we can conclude that `b` is true.
More concisely: If `a` and `b` are propositions, then `a -> b` holds when `(~a || b)` is true.
|
Nat.succ_pos
theorem Nat.succ_pos : ∀ (n : ℕ), 0 < n.succ
This theorem states that for every natural number `n`, the succeeding number (`Nat.succ n`) is greater than zero. In other words, the successor of any natural number is always positive.
More concisely: For every natural number `n`, `Nat.succ n` is positive. (Alternatively, `Nat.succ n` > 0.)
|
congrFun
theorem congrFun : ∀ {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
This theorem, named `congrFun`, states that if two functions `f` and `g` are equal (denoted as `f = g`), then the result of applying these functions to the same argument `a` will also be equal (denoted as `f a = g a`). These functions `f` and `g` are from a sort `α` to a sort `β`, where `β` itself is a function of `α`. This theorem holds for any sort `α` and `β` and any functions `f` and `g` of the specified type, and any element `a` of sort `α`.
More concisely: If two functions `f` and `g` from sort `α` to a function of `α` `β` are equal, then `f x = g x` for all `x` in `α`.
|