ContinuousOn.comp_fract'
theorem ContinuousOn.comp_fract' :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : LinearOrderedRing α] [inst_1 : FloorRing α]
[inst_2 : TopologicalSpace α] [inst_3 : OrderTopology α] [inst_4 : TopologicalSpace β]
[inst_5 : TopologicalSpace γ] {f : β → α → γ},
ContinuousOn (Function.uncurry f) (Set.univ ×ˢ Set.Icc 0 1) →
(∀ (s : β), f s 0 = f s 1) → Continuous fun st => f st.1 (Int.fract st.2)
The theorem `ContinuousOn.comp_fract'` states that for any three types `α`, `β`, and `γ` where `α` is a linearly ordered ring with a floor ring and a topology that is an order topology, and `β` and `γ` are topological spaces, given a function `f` mapping from `β` to `α` to `γ`, if `f` is continuous on the product of the universal set and the closed interval from 0 to 1, and for all `s` in `β`, `f` of `s` at 0 equals `f` of `s` at 1, then the function which maps a pair `st` to `f` of `st.1` at the fractional part of `st.2` is continuous. In other words, if `f` is continuous on a rectangular region in `β` x `α` and periodic in the `α` direction with period 1, then we can extend `f` to a continuous function on the 'wrapped' domain where we identify 0 and 1 in the `α` direction.
More concisely: If a continuous, periodically function `f` on a product of a linearly ordered ring `α` with a floor ring, an order topology, and a topological space `β`, satisfies `f(s, a) = f(s, b)` for all `s ∈ β` and `a, b ∈ α` with `b - a = 1`, then the function that maps `(s, x)` to `f(s, ⌊x⌋)` is continuous on `β x α`.
|
ContinuousOn.comp_fract''
theorem ContinuousOn.comp_fract'' :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedRing α] [inst_1 : FloorRing α] [inst_2 : TopologicalSpace α]
[inst_3 : OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β},
ContinuousOn f (Set.Icc 0 1) → f 0 = f 1 → Continuous (f ∘ Int.fract)
This theorem states that if a function `f` from a linearly ordered ring `α` to a topological space `β` is continuous on the closed interval from 0 to 1, and the function `f` has the same values at the endpoints 0 and 1, then the composition of the function `f` with the fractional part function (`Int.fract`) is a continuous function. The fractional part function is defined as the difference between a number and its floor (the greatest integer less than or equal to the number).
More concisely: If `f` is a continuous function from a linearly ordered ring `α` to a topological space `β` such that `f` is equal to `f`(0) at 0 and `f` is equal to `f`(1) at 1, then the composition of `f` and the fractional part function is continuous.
|