Real.isBounded_iff_bddBelow_bddAbove
theorem Real.isBounded_iff_bddBelow_bddAbove : ∀ {s : Set ℝ}, Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s := by
sorry
The theorem `Real.isBounded_iff_bddBelow_bddAbove` states that for any set `s` of real numbers, the set is bounded with respect to the ambient bornology (a structure that specifies which sets are "bounded") if and only if the set is bounded both below and above. In other words, a set of real numbers is considered bounded in this context if there exists both a lower bound and an upper bound for the set.
More concisely: A set of real numbers is bounded with respect to the ambient bornology if and only if it has both a lower bound and an upper bound.
|
Function.Periodic.isBounded_of_continuous
theorem Function.Periodic.isBounded_of_continuous :
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℝ → α} {c : ℝ},
Function.Periodic f c → c ≠ 0 → Continuous f → Bornology.IsBounded (Set.range f)
This theorem states that for any real-valued function `f` that is both continuous and periodic with a non-zero period `c`, the range of `f` is bounded. This is expressed in the context of a pseudometric space, which is a generalized metric space that allows for 'distance' between points to be zero even if the points are not identical. Thus, if `f` is a continuous, periodic function with a non-zero period, then the set of all its possible outputs (i.e., its range) is a bounded set according to the constraints of the underlying bornology (a mathematical structure that defines what it means for a subset to be 'bounded').
More concisely: If `f` is a continuous and periodic real-valued function with a non-zero period, then the range of `f` is a bounded set.
|
Int.tendsto_zmultiplesHom_cofinite
theorem Int.tendsto_zmultiplesHom_cofinite :
∀ {a : ℝ}, a ≠ 0 → Filter.Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (Filter.cocompact ℝ)
This theorem states that for any nonzero real number `a`, the function defined by the multiples of `a` (`zmultiplesHom` function) from integers (`ℤ`) to real numbers (`ℝ`) has a particular limit property: it is discrete in the sense that the inverse images of compact sets under this function are finite. In other words, if you take any compact set in the real numbers, the set of integers that map into this compact set under multiples of `a` is always a finite set. This is formalized by saying that the function `zmultiplesHom ℝ a` tends to the cofinite filter in the integers and to the cocompact filter in the real numbers. This is indicated by the `Filter.Tendsto` predicate.
More concisely: For any nonzero real number `a`, the function mapping integers to their multiples by `a` maps compact subsets of the real numbers to finite subsets of the integers.
|
Int.tendsto_coe_cofinite
theorem Int.tendsto_coe_cofinite : Filter.Tendsto Int.cast Filter.cofinite (Filter.cocompact ℝ)
The theorem `Int.tendsto_coe_cofinite` states that under the coercion from the set of integers `ℤ` to the set of real numbers `ℝ`, the inverse images of compact sets are finite. This is expressed in the language of filters, using the `Filter.Tendsto` function. It asserts that when integers are cast to real numbers via `Int.cast`, the preimage of any set in the cofinite filter (i.e., sets whose complements are finite) is in the cocompact filter of real numbers (i.e., sets whose complements are compact).
More concisely: The theorem `Int.tendsto_coe_cofinite` in Lean 4 asserts that the inverse image of any cofinite set under the coercion from integers to real numbers is a compact set.
|
AddSubgroup.tendsto_zmultiples_subtype_cofinite
theorem AddSubgroup.tendsto_zmultiples_subtype_cofinite :
∀ (a : ℝ), Filter.Tendsto (⇑(AddSubgroup.zmultiples a).subtype) Filter.cofinite (Filter.cocompact ℝ)
The theorem `AddSubgroup.tendsto_zmultiples_subtype_cofinite` states that for any real number `a`, the function that maps to the subgroup generated by 'multiples of `a`' (`AddSubgroup.zmultiples a`) converges to the filter of complements to compact sets in the real numbers (`Filter.cocompact ℝ`) when considered from the domain of the filter of subsets whose complements are finite (`Filter.cofinite`). In simpler terms, it indicates that the discrete subgroup generated by any real number `a` intersects with compact sets in a finite manner.
More concisely: The map from the filter of subsets of real numbers whose complements are finite to the filter of subgroups generated by multiples of a real number tends to the filter of complements of compact sets.
|
Function.Periodic.compact_of_continuous
theorem Function.Periodic.compact_of_continuous :
∀ {α : Type u} [inst : TopologicalSpace α] {f : ℝ → α} {c : ℝ},
Function.Periodic f c → c ≠ 0 → Continuous f → IsCompact (Set.range f)
The theorem states that for any real-valued function `f`, if `f` is both continuous and periodic with a non-zero period `c`, then the range of `f` is a compact set. Here, a function is said to be periodic with period `c` if for all real numbers `x`, `f (x + c) = f x`. The term "compact" in a topological space refers to a property that for every nontrivial filter `f` that contains the set, there exists an element of the set such that every set of `f` meets every neighborhood of that element. In simpler words, the theorem says that the set of all output values of a continuous, non-constant periodic function forms a compact set.
More concisely: If a real-valued, continuous, and non-constant function `f` has a finite, non-zero period `c`, then the range of `f` is a compact set.
|