Mathlib.Data.Int.Interval._auxLemma.2
theorem Mathlib.Data.Int.Interval._auxLemma.2 : ∀ {n m : ℕ}, (m ∈ Finset.range n) = (m < n)
This theorem states that for all natural numbers `n` and `m`, `m` is an element of the set of natural numbers less than `n` (represented by `Finset.range n` in Lean 4) if and only if `m` is strictly less than `n`. In other words, it establishes an equivalence between the membership of `m` in the set defined by `Finset.range n` and the inequality `m < n`.
More concisely: For all natural numbers `n` and `m`, `m` is in the finite set `{i | i < n}` if and only if `m` is strictly less than `n`.
|
Mathlib.Data.Int.Interval._auxLemma.3
theorem Mathlib.Data.Int.Interval._auxLemma.3 : ∀ {n : ℕ} {a : ℤ}, (n < a.toNat) = (↑n < a)
The given theorem, `Mathlib.Data.Int.Interval._auxLemma.3`, states that for all natural numbers `n` and all integers `a`, `n` is less than the natural number equivalent of `a` if and only if `n` as an integer is less than `a`. In other words, a natural number `n` is less than the natural number representation of an integer `a` precisely when `n`, considered as an integer, is also less than `a`. This theorem essentially provides a bridge between the natural and integer number systems for comparison operations.
More concisely: For all natural numbers n and integers a, n < nat_of_int a if and only if n < a.
|
Mathlib.Data.Int.Interval._auxLemma.1
theorem Mathlib.Data.Int.Interval._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {b : β}, (b ∈ Finset.map f s) = ∃ a ∈ s, f a = b := by
sorry
This theorem asserts that for any types `α` and `β`, an embedding `f` from `α` into `β`, a finite set `s` of type `α`, and an element `b` of type `β`, the condition `b ∈ Finset.map f s` is equivalent to the existence of an element `a` in `s` such that `f a = b`. In other words, `b` belongs to the image of `s` under `f` if and only if `b` is the image of some element in `s`.
More concisely: For any types `α` and `β`, an embedding `f` from `α` to `β`, and a finite set `s` in `α`, the element `b` is in the image of `s` under `f` if and only if there exists `a` in `s` such that `f(a) = b`.
|
Int.card_Icc
theorem Int.card_Icc : ∀ (a b : ℤ), (Finset.Icc a b).card = (b + 1 - a).toNat
The theorem `Int.card_Icc` states that for any two integers `a` and `b`, the cardinality (or the number of elements) of the finite set that includes all integers `x` such that `a ≤ x` and `x ≤ b` (represented by `Finset.Icc a b`), is equal to the natural number equivalent of the integer result of the operation `(b + 1 - a)`. If `b + 1 - a` is negative, the cardinality will be treated as zero, as negative integers are converted to zero when they are turned into a natural number using the `Int.toNat` function.
More concisely: The cardinality of the finite set of integers between `a` and `b` (inclusive) is equal to `(b - a + 1)`. If `b < a`, the cardinality is considered zero.
|