unitInterval.symm.proof_1
theorem unitInterval.symm.proof_1 : ∀ (t : ↑unitInterval), 1 - ↑t ∈ unitInterval
This theorem states that for every real number `t` in the unit interval `[0,1]`, the number `1 - t` is also in the unit interval. In other words, if you subtract any number from the unit interval `[0,1]` from `1`, the result will still be within the unit interval `[0,1]`.
More concisely: For every real number `t` in the interval `[0, 1]`, `1 - t` also belongs to the interval `[0, 1]`.
|
unitInterval.symm_zero
theorem unitInterval.symm_zero : unitInterval.symm 0 = 1
This theorem states that the central symmetry of the unit interval at the point 0 yields the value 1. In other words, under the operation defined by the function `unitInterval.symm`, which maps each point in the unit interval to its symmetric counterpart with respect to the center of the interval, the point 0 is mapped to the point 1.
More concisely: The central symmetry of the unit interval maps point 0 to point 1. (In Lean: `unit_interval.symm 0 = 1`)
|
exists_monotone_Icc_subset_open_cover_unitInterval
theorem exists_monotone_Icc_subset_open_cover_unitInterval :
∀ {ι : Sort u_1} {c : ι → Set ↑unitInterval},
(∀ (i : ι), IsOpen (c i)) →
Set.univ ⊆ ⋃ i, c i →
∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
This theorem states that given any collection of open sets (indexed by `ι`) that cover the entire unit interval in real numbers (i.e., from 0 to 1 inclusive), there exists a sequence `t` of real numbers starting at 0 that is monotone (non-decreasing) such that, beyond some point `n`, `t m` equals 1 for all `m ≥ n`. Furthermore, for every natural number `n`, there is an index `i` such that the closed interval from `t n` to `t (n + 1)` is entirely contained within the `i`-th set in the collection. In other words, the open cover of the unit interval can be refined into a finite partition of closed subintervals, each of which is contained within one of the original open sets.
More concisely: Given any open cover of the real unit interval, there exists a monotone sequence t in [0,1] and a finite subcollection of sets from the cover such that each set contains exactly one subinterval [tn, t(n+1)] of the sequence.
|
unitInterval.symm_symm
theorem unitInterval.symm_symm : ∀ (x : ↑unitInterval), unitInterval.symm (unitInterval.symm x) = x
This theorem states that for any real number `x` in the unit interval `[0,1]`, applying the function `unitInterval.symm` twice returns the original number. In other words, `unitInterval.symm` is its own inverse when restricted to the unit interval in the real numbers.
More concisely: For any real number `x` in the unit interval `[0,1]`, `unitInterval.symm x = x`.
|
unitInterval.nonneg'
theorem unitInterval.nonneg' : ∀ {t : ↑unitInterval}, 0 ≤ t
This theorem, named `unitInterval.nonneg'`, states that for all real numbers `t` that belong to the unit interval (i.e., the interval from 0 to 1 inclusive), `t` is greater than or equal to 0. In other words, no number in the unit interval is negative.
More concisely: For all real numbers `t`, if 0 ≤ t ≤ 1 then t ≥ 0. (The unit interval includes 0, so an alternative statement is: For all real numbers `t`, if 0 ≤ t then t ≥ 0.)
|
unitInterval.two_mul_sub_one_mem_iff
theorem unitInterval.two_mul_sub_one_mem_iff : ∀ {t : ℝ}, 2 * t - 1 ∈ unitInterval ↔ t ∈ Set.Icc (1 / 2) 1
The theorem `unitInterval.two_mul_sub_one_mem_iff` states that for any real number `t`, `2 * t - 1` lies in the unit interval (which is the set of real numbers between 0 and 1 inclusive) if and only if `t` itself lies in the closed interval from `1/2` to `1` (inclusive). This provides a useful characterization of when a transformation of a real number falls within the unit interval in terms of limits on the original number.
More concisely: For any real number `t`, `2 * t - 1` is in the unit interval if and only if `t` is between 1/2 and 1.
|
unitInterval.mul_pos_mem_iff
theorem unitInterval.mul_pos_mem_iff : ∀ {a t : ℝ}, 0 < a → (a * t ∈ unitInterval ↔ t ∈ Set.Icc 0 (1 / a))
The theorem `unitInterval.mul_pos_mem_iff` states that for all real numbers `a` and `t`, given `a` is greater than 0, the product `a * t` belongs to the unit interval (i.e., the closed interval from 0 to 1) if and only if `t` belongs to the closed interval from 0 to `1 / a`. This theorem provides a connection between multiplication by a positive real number and membership in certain real number intervals.
More concisely: For a positive real number `a` and any real number `t`, `a * t` belongs to the unit interval if and only if `t` is in the closed interval [0, 1/a].
|
unitInterval.le_one'
theorem unitInterval.le_one' : ∀ {t : ↑unitInterval}, t ≤ 1
This theorem, referred to as `unitInterval.le_one'`, asserts that for all real numbers `t` that belong to the set of real numbers defined as the unit interval (denoted by `unitInterval` and defined as the closed interval from 0 to 1 in real numbers), the value of `t` is less than or equal to 1. The inequality is contained within the interval `I`. In other words, this theorem states that any number within the unit interval is always less than or equal to 1.
More concisely: For all real numbers `t`, if `t` belongs to the unit interval [0,1], then `t` ≤ 1.
|
unitInterval.continuous_symm
theorem unitInterval.continuous_symm : Continuous unitInterval.symm
This theorem states that the function `unitInterval.symm`, which represents the central symmetry on the unit interval (mapping each point to its "mirror image" around the midpoint 0.5), is a continuous function. In more mathematical terms, for any point `t` in the unit interval, the function that maps `t` to `1 - t` is continuous on the entire interval [0,1].
More concisely: The central symmetry function `unitInterval.symm` (mapping `t` to `1 - t`) is a continuous function on the unit interval [0,1].
|
Set.abs_projIcc_sub_projIcc
theorem Set.abs_projIcc_sub_projIcc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c d : α} (h : a ≤ b),
|↑(Set.projIcc a b h c) - ↑(Set.projIcc a b h d)| ≤ |c - d|
The theorem `Set.abs_projIcc_sub_projIcc` states that for any linearly ordered additive commutative group `α`, and any elements `a`, `b`, `c`, `d` of `α` where `a ≤ b`, the absolute difference between the projections (`Set.projIcc`) of `c` and `d` onto the closed interval [`a`, `b`] is less than or equal to the absolute difference between `c` and `d`. This means that projection onto the interval [`a`, `b`] does not increase the distance between any two points in `α`, making `Set.projIcc` a contraction.
More concisely: For any linearly ordered additive commutative group `α` and elements `a ≤ b` in `α`, the absolute difference between the projections of `c` and `d` onto the interval [`a`, `b`] is less than or equal to the absolute difference between `c` and `d` for all `c`, `d` in `α`.
|
affineHomeomorph_image_I
theorem affineHomeomorph_image_I :
∀ {𝕜 : Type u_1} [inst : LinearOrderedField 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : TopologicalRing 𝕜] (a b : 𝕜)
(h : 0 < a), ⇑(affineHomeomorph a b ⋯) '' Set.Icc 0 1 = Set.Icc b (a + b)
The theorem `affineHomeomorph_image_I` states that for any type `𝕜`, given it is a linear ordered field and has a structure of a topological space and a topological ring, if we take any two elements `a` and `b` from `𝕜` where `a` is greater than zero, then the image of the interval `[0,1]` under the homeomorphism defined by the function `x ↦ a * x + b` is the interval `[b, a+b]`. In simpler terms, if you transform the interval from 0 to 1 by multiplying it by `a` and then adding `b`, you get the interval from `b` to `a+b`.
More concisely: For any linear ordered field `𝕜` with a topological space and ring structure, the image of the interval `[0, 1]` under the affine homeomorphism `x ↦ a * x + b` is `[b, a + b]`, where `a` is a positive element in `𝕜`.
|
exists_monotone_Icc_subset_open_cover_Icc
theorem exists_monotone_Icc_subset_open_cover_Icc :
∀ {ι : Sort u_1} {a b : ℝ},
a ≤ b →
∀ {c : ι → Set ↑(Set.Icc a b)},
(∀ (i : ι), IsOpen (c i)) →
Set.univ ⊆ ⋃ i, c i →
∃ t,
↑(t 0) = a ∧
Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
This theorem states that for any open cover `c` of a closed interval `[a, b]` in the real numbers, where `a` is less than or equal to `b`, there exists a function `t` that partitions `[a, b]` into finite subintervals such that `t` is a monotone function and its range starting from a certain natural number `m` is exactly `b`. Each subinterval of the partition is contained within some set of the open cover `c`. An open cover is a family of open sets whose union contains the covered set, in this case the interval `[a, b]`. A subset is refined by the partition if every set in the original collection contains at least one set in the refining collection. Monotone refers to the property of a function that preserves the given order or relation.
More concisely: For any open cover of a closed interval in the real numbers, there exists a monotone function that partitions the interval with subintervals contained in the cover and whose range starts from some natural number and includes the upper endpoint of the interval.
|
unitInterval.symm_one
theorem unitInterval.symm_one : unitInterval.symm 1 = 0
The theorem `unitInterval.symm_one` states that the central symmetry function of the unit interval, when applied to the endpoint 1, yields the opposite endpoint 0. In other words, the symmetry function reflects the unit interval about its center, and hence mapping 1 to 0.
More concisely: The central symmetry function of the unit interval maps 1 to 0.
|
unitInterval.nonneg
theorem unitInterval.nonneg : ∀ (x : ↑unitInterval), 0 ≤ ↑x
The theorem `unitInterval.nonneg` states that for every element `x` in the set `unitInterval`, which represents the closed interval from 0 to 1 in ℝ (real numbers), `x` is greater than or equal to 0. In other words, all elements in the `unitInterval` are nonnegative real numbers.
More concisely: For all x in the real numbers, if x is an element of the unit interval [0, 1], then x ≥ 0.
|