Fin.pos
theorem Fin.pos : ∀ {n : ℕ}, Fin n → 0 < n
This theorem, `Fin.pos`, states that for all natural numbers `n`, if there exists a value in the `Fin n` type, then `n` must be greater than zero. In mathematical terms, if `n` is a natural number that can be indexed into a finite set (i.e., `n` is in `Fin n`), then `n` must be positive. The `Fin n` type in Lean represents a finite set of `n` elements, so if `n` were zero, there would be no elements, contradicting the assumption.
More concisely: For any natural number `n`, if `n` is an element of `Fin n`, then `n` is positive.
|
Fin.cast.proof_1
theorem Fin.cast.proof_1 : ∀ {n m : ℕ}, n = m → ∀ (i : Fin n), ↑i < m
This theorem states that for any two natural numbers `n` and `m`, if `n` equals `m`, then for any `i` in the finite set of `n`, the value of `i` is less than `m`. In other words, every element of a finite set of size `n` is less than `n` itself.
More concisely: For any finite set of natural numbers of size `n`, every element `i` in the set satisfies `i < n`.
|
Fin.val_lt_of_le
theorem Fin.val_lt_of_le : ∀ {n b : ℕ} (i : Fin b), b ≤ n → ↑i < n
This theorem states that for any two natural numbers `n` and `b`, and any `i` which is a finite subtype of `b`, if `b` is less than or equal to `n`, then the casting of `i` to a natural number is strictly less than `n`. In other words, it asserts that if a number is within the bounds of a smaller natural number, it must be strictly less than a larger one it is compared to.
More concisely: If `i` is a finite subtype of natural number `b` and `b` is less than or equal to natural number `n`, then the natural number cast of `i` is strictly less than `n`.
|