LocallyFiniteOrderBot.finset_mem_Iio
theorem LocallyFiniteOrderBot.finset_mem_Iio :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrderBot α] (a x : α),
x ∈ LocallyFiniteOrderBot.finsetIio a ↔ x < a
The theorem `LocallyFiniteOrderBot.finset_mem_Iio` states that for any type `α` that has a preorder relation and is a locally finite order at the bottom (`LocallyFiniteOrderBot`), for any elements `a` and `x` of `α`, `x` is an element of the left-infinite right-open interval ending at `a` (`finsetIio a`) if and only if `x` is less than `a`. In simpler terms, an element `x` belongs to the set of all elements less than `a` if and only if `x` is indeed less than `a`.
More concisely: For any locally finite order type `α` with bottom element, an element `x` belongs to the left-infinite right-open interval `finsetIio a` if and only if `x` is strictly less than `a`.
|
Finset.mem_Ioc
theorem Finset.mem_Ioc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
The theorem `Finset.mem_Ioc` states that for any types `α` with a preorder and a locally finite order, and any elements `a`, `b`, and `x` of `α`, `x` is a member of the finite set `Finset.Ioc a b` if and only if `a` is less than `x` and `x` is less than or equal to `b`. In other words, `x` belongs to the interval `(a, b]` in `α`.
More concisely: For any type `α` with a preorder and locally finite order, `x` belongs to the interval `(a, b]` if and only if `a` is strictly less than `x` and `x` is less than or equal to `b`.
|
Finset.mem_uIcc
theorem Finset.mem_uIcc :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
x ∈ Finset.uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b
This theorem is about membership in the set `Finset.uIcc a b` in a lattice. It states that for any type `α` that has a lattice structure and a locally finite order, and for any elements `a`, `b`, and `x` of this type, `x` is an element of `Finset.uIcc a b` if and only if `x` is greater than or equal to the meet of `a` and `b` (denoted `a ⊓ b`) and less than or equal to the join of `a` and `b` (denoted `a ⊔ b`). In other words, `x` lies within the "bounding box" formed by `a` and `b`, inclusive.
More concisely: For any type `α` with a lattice structure and a locally finite order, `x` is an element of `Finset.uIcc a b` if and only if `a ⊓ b ≤ x ≤ a ⊔ b`.
|
Finset.coe_Iic
theorem Finset.coe_Iic :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α), ↑(Finset.Iic a) = Set.Iic a := by
sorry
The theorem `Finset.coe_Iic` states that for any type `α` that has a preorder and is a locally finite order at the bottom (those where every bounded below set has an infimum), and for any element `a` of type `α`, the coercion of the finite set of elements `x` such that `x` is less than or equal to `a` (denoted as `Finset.Iic a`) into a set is equal to the left-infinite, right-closed interval of all `x` in `α` such that `x` is less than or equal to `a` (denoted as `Set.Iic a`). In other words, the function `Finset.coe_Iic` asserts the equivalence of the finite set and the infinite set representations of an interval bounded on one side.
More concisely: The theorem `Finset.coe_Iic` asserts that the coercion of the finite set of elements less than or equal to an element `a` in a locally finite order type `α` is equal to the left-infinite, right-closed interval of elements less than or equal to `a` in `α`.
|
Set.finite_Icc
theorem Set.finite_Icc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), (Set.Icc a b).Finite
The theorem `Set.finite_Icc` states that for any given type `α` with a preorder (that is, a binary relation that is reflexive and transitive) and a locally finite order (an order with finitely many elements between any two elements), the closed interval `[a, b]` (denoted as `Set.Icc a b`), with `a` and `b` being elements of `α`, is a finite set. This means there exists a natural number `n` such that there is an equivalence between the interval `[a, b]` and the set of first `n` natural numbers (including 0).
More concisely: For any type `α` with a preorder and locally finite order, the closed interval `[a, b]` in `α` is a finite set.
|
LocallyFiniteOrderBot.finset_mem_Iic
theorem LocallyFiniteOrderBot.finset_mem_Iic :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrderBot α] (a x : α),
x ∈ LocallyFiniteOrderBot.finsetIic a ↔ x ≤ a
The theorem `LocallyFiniteOrderBot.finset_mem_Iic` states that for any types `α` with a preorder and `LocallyFiniteOrderBot`, and for any elements `a` and `x` of type `α`, `x` is an element of the finset `Iic a` (which essentially represents the interval from negative infinity to `a`, inclusive) if and only if `x` is less than or equal to `a`. This theorem is a formalization in Lean 4 of the relation between a value and a right-closed interval.
More concisely: For any type `α` with a preorder and `LocallyFiniteOrderBot`, and for any elements `a` and `x` of type `α`, `x` is in the interval `Iic a` if and only if `x` is less than or equal to `a`.
|
LocallyFiniteOrder.finset_mem_Icc
theorem LocallyFiniteOrder.finset_mem_Icc :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrder α] (a b x : α),
x ∈ LocallyFiniteOrder.finsetIcc a b ↔ a ≤ x ∧ x ≤ b
This theorem, `LocallyFiniteOrder.finset_mem_Icc`, states that for any given type `α` that has a preorder relationship and is locally finite, and for any elements `a`, `b`, and `x` of type `α`, `x` belongs to the finite set that forms a closed interval from `a` to `b` if and only if `x` is greater than or equal to `a` and less than or equal to `b`. In other words, it describes the membership relation of an element `x` in the left-closed right-closed interval from `a` to `b`, denoted as `[a, b]`, in a locally finite ordered set.
More concisely: For any locally finite ordered set `α` and elements `a ≤ b` in `α`, the element `x ∈ α` belongs to the interval `[a, b]` if and only if `a ≤ x ≤ b`.
|
Finset.mem_Icc
theorem Finset.mem_Icc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
This theorem asserts that for any type `α` that has a preorder (i.e., a binary relation that is reflexive and transitive) and a locally finite order (i.e., every bounded interval is finite), and for any three elements `a`, `b`, `x` of this type, `x` belongs to the finite set of elements between `a` and `b` (inclusive) if and only if `x` is greater than or equal to `a` and less than or equal to `b`. In other words, `x` is in the set `Finset.Icc a b` precisely when `a ≤ x ≤ b`.
More concisely: For any type `α` with a reflexive, transitive preorder and finite intervals, an element `x` lies between `a` and `b` if and only if `a ≤ x ≤ b`.
|
Finset.mem_Ioi
theorem Finset.mem_Ioi :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Finset.Ioi a ↔ a < x := by
sorry
The theorem `Finset.mem_Ioi` states that for any type `α` that has a preorder and a locally finite order top, and for any elements `a` and `x` of that type, `x` is an element of the finset `Ioi a` (which is the finset of elements greater than `a`) if and only if `a` is less than `x`. This theorem essentially provides a characterization of the membership of the finset `Ioi a` in terms of the less than relation.
More concisely: For any type `α` with a preorder and locally finite order top, `x` is an element of the finset `Ioi a` if and only if `a` is strictly less than `x`.
|
LocallyFiniteOrder.finset_mem_Ioc
theorem LocallyFiniteOrder.finset_mem_Ioc :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrder α] (a b x : α),
x ∈ LocallyFiniteOrder.finsetIoc a b ↔ a < x ∧ x ≤ b
This theorem, `LocallyFiniteOrder.finset_mem_Ioc`, states that for any type `α` with a preorder and locally finite order, and any elements `a`, `b`, and `x` of type `α`, the element `x` is in the left-open right-closed interval from `a` to `b` (denoted as `LocallyFiniteOrder.finsetIoc a b`) if and only if `a` is less than `x` and `x` is less than or equal to `b`. This theorem essentially provides a criterion for membership in this specific type of interval in terms of the standard ordering on the underlying type.
More concisely: For any type `α` with locally finite order and preorder, an element `x` belongs to the left-open right-closed interval `[a, b]` if and only if `a < x <= b`.
|
Finset.coe_Iio
theorem Finset.coe_Iio :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α), ↑(Finset.Iio a) = Set.Iio a := by
sorry
This theorem states that for any type `α` that has a preorder (meaning `α` has a binary relation that is reflexive and transitive) and a locally finite order with a bottom element, the coersion of the finset `Iio a` (which is a set of elements `x` such that `x` is less than `a`) is equal to the set `Iio a` (which is a left-infinite right-open interval, meaning it includes all elements less than `a` but not `a` itself). In other words, the elements of the finset `Iio a` make up exactly the set `Iio a`.
More concisely: For any type `α` with a preorder, locally finite order, and a bottom element, the coercion of the finset `Iio a` equals the set of elements strictly less than `a`.
|
LocallyFiniteOrder.finset_mem_Ioo
theorem LocallyFiniteOrder.finset_mem_Ioo :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrder α] (a b x : α),
x ∈ LocallyFiniteOrder.finsetIoo a b ↔ a < x ∧ x < b
This theorem states that for any type `α` with a preorder and a locally finite order, and given elements `a`, `b`, and `x` of this type, `x` belongs to the left-open right-open interval between `a` and `b` if and only if `a` is less than `x` and `x` is less than `b`. In other words, the theorem provides a characterization of membership in a locally finite, left-open right-open interval in terms of strict inequalities.
More concisely: For any type `α` with a preorder and locally finite order, an element `x` lies between `a` and `b` if and only if `a` is strictly less than `x` and `x` is strictly less than `b`.
|
Finset.mem_Ici
theorem Finset.mem_Ici :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Finset.Ici a ↔ a ≤ x := by
sorry
This theorem, `Finset.mem_Ici`, states that for any type `α` that has a preorder (an order that is reflexive and transitive) and is a locally finite order (an order where every interval is finite), and for any elements `a` and `x` of type `α`, `x` is an element of the finset `Ici a` if and only if `a` is less than or equal to `x`. Here, `Ici a` represents the finset of all elements `x` such that `a ≤ x`. So, this theorem essentially provides a criterion for membership in the finset `Ici a`.
More concisely: For any type `α` with a preorder and the locally finite order property, `x` is an element of the finset `Ici a` if and only if `a ≤ x`.
|
Finset.coe_Ici
theorem Finset.coe_Ici :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), ↑(Finset.Ici a) = Set.Ici a := by
sorry
This theorem states that for any type `α` (assumed to have a preorder and locally finite order-top structure) and any element `a` of type `α`, the coercion of the finset of all elements greater than or equal to `a` (`Finset.Ici a`) to a set is equal to the set of all elements greater than or equal to `a` (`Set.Ici a`). In other words, the set of elements in the finset that are greater than or equal to a given value `a` is the same as the set of all elements in the type that are greater than or equal to `a`.
More concisely: For any type `α` with preorder and locally finite order-topology, and any `a` in `α`, the set `{x : α | x ≥ a}` is equal to the finset `Finset.Ici a`.
|
Finset.mem_Iio
theorem Finset.mem_Iio :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a x : α}, x ∈ Finset.Iio a ↔ x < a := by
sorry
This theorem states that for any types `α`, which has preorder and locally finite order bot structure, and any elements `a` and `x` of type `α`, `x` is an element of the `Finset.Iio a` if and only if `x` is less than `a`. Here, `Finset.Iio a` refers to the finite set of elements `x` such that `x` is less than `a`.
More concisely: For any type `α` with preorder and locally finite order bot structure, an element `x` lies in the finite set `Finset.Iio a` if and only if `x` is less than `a`.
|
Finset.mem_Iic
theorem Finset.mem_Iic :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a x : α}, x ∈ Finset.Iic a ↔ x ≤ a := by
sorry
This theorem states that for any given type `α` which has a preorder and a locally finite order bot, and any elements `a` and `x` of this type, `x` is a member of the finite set `Finset.Iic a` if and only if `x` is less than or equal to `a`. In other words, it formalizes the intuition that `Finset.Iic a` contains exactly those elements `x` which satisfy `x ≤ a`.
More concisely: For any type `α` with a preorder and locally finite order bottom element, `x` belongs to the interval `Finset.Iic a` if and only if `x ≤ a`.
|
Finset.mem_Ico
theorem Finset.mem_Ico :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
x ∈ Finset.Ico a b ↔ a ≤ x ∧ x < b
The theorem `Finset.mem_Ico` states that for any type `α` which has a preorder and a locally finite order, and for any elements `a`, `b`, and `x` of type `α`, `x` is in the finset `Ico` from `a` to `b` if and only if `x` is greater than or equal to `a` and less than `b`. In other words, an element `x` belongs to the finset of elements between `a` and `b` (inclusive of `a` and exclusive of `b`) if and only if `a ≤ x < b`.
More concisely: For any type `α` with a preorder and locally finite order, an element `x` lies in the finset `Ico` from `a` to `b` if and only if `a ≤ x < b`.
|
Finset.coe_Ioi
theorem Finset.coe_Ioi :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), ↑(Finset.Ioi a) = Set.Ioi a := by
sorry
The theorem `Finset.coe_Ioi` is stating that for any type `α` which has a preorder relation and a locally finite order, for any element `a` of that type, the coercion of the finset of elements greater than `a` (expressed as `Finset.Ioi a`) is equal to the set of elements greater than `a` (expressed as `Set.Ioi a`). Essentially, this theorem establishes the equivalence between a certain finset and a certain set in the given context.
More concisely: For any type `α` with a preorder and locally finite order, `Finset.Ioi a = Set.Ioi a`. That is, the coercion of the finset of elements greater than `a` is equal to the set of elements greater than `a`.
|
Finset.mem_Ioo
theorem Finset.mem_Ioo :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α},
x ∈ Finset.Ioo a b ↔ a < x ∧ x < b
The theorem `Finset.mem_Ioo` states that for any type `α` that has a preorder and is a locally finite order, and for any elements `a`, `b`, and `x` of this type, `x` is in the finite set defined by the interval `(a,b)` (exclusive) if and only if `a` is less than `x` and `x` is less than `b`. This means that `a < x < b` is the criteria for membership in the finite set `Finset.Ioo a b`.
More concisely: For any locally finite preordered type $\alpha$, and any $a, b \in \alpha$ with $a < b$, the element $x \in \alpha$ belongs to the open interval $(a, b)$ if and only if $a < x < b$.
|
Finset.coe_Ioc
theorem Finset.coe_Ioc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Ioc a b) = Set.Ioc a b
This theorem states that for any type `α` which has a preorder and a locally finite order, and for any two elements `a` and `b` of this type, the set obtained by coercing the finite set of elements greater than `a` and less than or equal to `b` (denoted `Finset.Ioc a b`) is equal to the set of elements in the left-open right-closed interval between `a` and `b` (denoted `Set.Ioc a b`). In other words, the coercion of the finite set interval is the same as the set interval in the given order.
More concisely: For any type with a preorder and locally finite order, the coercion of the finite set interval between two elements is equal to the set interval.
|
LocallyFiniteOrder.finset_mem_Ico
theorem LocallyFiniteOrder.finset_mem_Ico :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrder α] (a b x : α),
x ∈ LocallyFiniteOrder.finsetIco a b ↔ a ≤ x ∧ x < b
The theorem `LocallyFiniteOrder.finset_mem_Ico` states that for any type `α` with a preorder, and under the condition that `α` has a locally finite order, an element `x` belongs to the left-closed right-open interval from `a` to `b`, denoted as `finsetIco a b`, if and only if `a` is less than or equal to `x` and `x` is strictly less than `b`. This theorem describes the membership condition for a specified interval in a locally finite ordered set.
More concisely: In a locally finite ordered set, an element belongs to the left-closed right-open interval [a, b) if and only if a <= x < b.
|
Finset.coe_Ioo
theorem Finset.coe_Ioo :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Ioo a b) = Set.Ioo a b
This theorem states that for any type `α` with a preorder and a locally finite order, and any two elements `a` and `b` of `α`, the finset of elements `x` such that `a < x` and `x < b` (denoted by `Finset.Ioo a b`) is equivalent to the set of elements `x` in `α` that are strictly greater than `a` and strictly less than `b` (denoted by `Set.Ioo a b`). In other words, the coercion of `Finset.Ioo a b` to a set gives us `Set.Ioo a b`.
More concisely: For any type `α` with a preorder and a locally finite order, the set of elements strictly between `a` and `b` equals the finite set of elements strictly less than `b` and strictly greater than `a`.
|
Finset.coe_Ico
theorem Finset.coe_Ico :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Ico a b) = Set.Ico a b
This theorem states that for any type `α` equipped with a preorder and a locally finite order, and any elements `a` and `b` of this type, the set obtained by coercing (or converting) the finite set of elements `x` such that `a ≤ x` and `x < b` (which is what `Finset.Ico a b` denotes) to a 'regular' set is equal to the set of elements `x` satisfying the same inequalities (which is what `Set.Ico a b` denotes). In other words, the interval `[a, b)` considered as a finite set and as a 'regular' set are the same.
More concisely: For any type `α` with a preorder and locally finite order, the finite interval `Finset.Ico a b` is equal to the regular interval `Set.Ico a b`.
|
Finset.coe_Icc
theorem Finset.coe_Icc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α), ↑(Finset.Icc a b) = Set.Icc a b
The theorem `Finset.coe_Icc` states that for any type `α` that has both a preorder and a locally finite order, and for any two elements `a` and `b` of this type, the coercion of the finite set interval (Finset.Icc) from `a` to `b` is equal to the set interval (Set.Icc) from `a` to `b`. In other words, it asserts that the set of elements in the interval from `a` to `b` (inclusive) as a finite set is the same as the interval from `a` to `b` (inclusive) as a set, under the conditions specified.
More concisely: For any type `α` with a preorder and locally finite order, the coercion of the finite set interval `Finset.Icc` from `a` to `b` equals the set interval `Set.Icc` from `a` to `b`.
|
LocallyFiniteOrderTop.finset_mem_Ioi
theorem LocallyFiniteOrderTop.finset_mem_Ioi :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrderTop α] (a x : α),
x ∈ LocallyFiniteOrderTop.finsetIoi a ↔ a < x
The theorem `LocallyFiniteOrderTop.finset_mem_Ioi` states that for any type `α` that has a predefined order (i.e., it has a `Preorder` instance) and is a locally finite order top (i.e., it has a `LocallyFiniteOrderTop` instance), and for any two elements `a` and `x` of this type, `x` belongs to the finset which is the left-open right-infinite interval starting from `a` if and only if `a` is strictly less than `x`. In other words, a member `x` is in the finset of elements greater than `a` if and only if `x` is truly greater than `a`. This theorem establishes a key property of the finset generated by the `LocallyFiniteOrderTop.finsetIoi` function.
More concisely: For any locally finite order top type `α` with a predefined order, an element `x` belongs to the finset of elements strictly greater than `a` if and only if `a` is strictly less than `x`.
|
LocallyFiniteOrderTop.finset_mem_Ici
theorem LocallyFiniteOrderTop.finset_mem_Ici :
∀ {α : Type u_1} [inst : Preorder α] [self : LocallyFiniteOrderTop α] (a x : α),
x ∈ LocallyFiniteOrderTop.finsetIci a ↔ a ≤ x
The theorem `LocallyFiniteOrderTop.finset_mem_Ici` states that for any type `α` with a preorder structure, under the context of a locally finite order topology, a given element `x` of `α` belongs to the finset `Ici a` (which represents a left-closed right-infinite interval starting from `a`) if and only if `a` is less than or equal to `x`. In other words, the theorem defines membership in a finset `Ici a` in terms of the preorder relationship.
More concisely: For any preordered type `α` and element `x` in `α` under a locally finite order topology, `x` belongs to the left-closed right-infinite interval `Ici a` if and only if `a ≤ x`.
|