NonemptyInterval.ext
theorem NonemptyInterval.ext : ∀ {α : Type u_7} {inst : LE α} (x y : NonemptyInterval α), x.toProd = y.toProd → x = y
This theorem states that for any type `α` with a less-than-or-equal-to relation, if we have two non-empty intervals `x` and `y` of `α`, then if the interval represented as a product by `toProd` function is the same for both `x` and `y`, then `x` and `y` must be the same interval. Essentially, it guarantees that two non-empty intervals are equal if they represent the same interval (as a product of lower and upper bounds).
More concisely: If `α` is a type with a total order and `x` and `y` are non-empty intervals of `α` with equal product representations, then `x = y`.
|
NonemptyInterval.coe_pure
theorem NonemptyInterval.coe_pure :
∀ {α : Type u_1} [inst : PartialOrder α] (a : α), ↑(NonemptyInterval.pure a) = {a}
This theorem states that for any type `α` that has a partial order, the function `NonemptyInterval.pure a` returns a non-empty interval that only contains the single element `a`. This function effectively creates an interval from `a` to `a`. As a result, when this interval is converted back to a set (using the coercion `↑`), it yields the singleton set containing only `a`. In other words, the "pure" non-empty interval containing `a` is equivalent to the singleton set `{a}`.
More concisely: For any type `α` with a partial order, the function `NonemptyInterval.pure a` is equivalent to the singleton set `{a}`.
|
NonemptyInterval.toDualProd_injective
theorem NonemptyInterval.toDualProd_injective :
∀ {α : Type u_1} [inst : LE α], Function.Injective NonemptyInterval.toDualProd
This theorem states that for any type `α` which has an order (`LE`), the function `NonemptyInterval.toDualProd` is injective. In other words, if we have two nonempty intervals in `α` and the function `NonemptyInterval.toDualProd` maps these two intervals to the same ordered pair of `α`, then these two intervals are the same. In simple terms, no two different nonempty intervals in `α` will give the same ordered pair when mapped by the function `NonemptyInterval.toDualProd`.
More concisely: For any type `α` with an order, the function `NonemptyInterval.toDualProd` maps distinct nonempty intervals in `α` to distinct ordered pairs.
|
NonemptyInterval.toProd_injective
theorem NonemptyInterval.toProd_injective :
∀ {α : Type u_1} [inst : LE α], Function.Injective NonemptyInterval.toProd
The theorem `NonemptyInterval.toProd_injective` states that for all types `α` that have an order relation `≤`, the function `toProd` which maps a non-empty interval of `α` to a pair of `α` values is injective. In other words, if two non-empty intervals in `α` are mapped to the same pair of `α` values by the `toProd` function, then those two non-empty intervals must be identical.
More concisely: If `α` is a type with an order relation `≤`, then the function `toProd` mapping non-empty intervals of `α` to pairs of `α` values is an injection.
|
NonemptyInterval.fst_le_snd
theorem NonemptyInterval.fst_le_snd :
∀ {α : Type u_7} [inst : LE α] (self : NonemptyInterval α), self.toProd.1 ≤ self.toProd.2
This theorem states that for any non-empty interval of a type `α` that has a less than or equal to (`≤`) operation, the first element (`fst`) of this interval is less than or equal to (`≤`) the second element (`snd`). In other words, the starting point of the interval is always less than or equal to its endpoint.
More concisely: For any interval `[a : α] [nonempty] [has_le a]`, we have `a ≤ a.2`.
|