English
The lemma expresses a general composition rule for fract with continuous on, showing continuity of the composite in a product space.
Русский
Лемма выражает общую композицию fract с непрерывностью on, доказывая непрерывность композиции в произведённом пространстве.
LaTeX
$$$$\text{ContinuousOn}(\text{uncurry } f, \text{domain}) \Rightarrow \text{Continuous}( (s,t) \mapsto f(s, \operatorname{fract}(t)) ).$$$$
Lean4
/-- Do not use this, use `ContinuousOn.comp_fract` instead. -/
theorem comp_fract' {f : β → α → γ} (h : ContinuousOn (uncurry f) <| univ ×ˢ I) (hf : ∀ s, f s 0 = f s 1) :
Continuous fun st : β × α => f st.1 (fract st.2) :=
by
change Continuous (uncurry f ∘ Prod.map id fract)
rw [continuous_iff_continuousAt]
rintro ⟨s, t⟩
rcases em (∃ n : ℤ, t = n) with (⟨n, rfl⟩ | ht)
· rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]
constructor
· refine
(((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
(tendsto_id.prodMap (tendsto_fract_left _))).mono_right
(le_of_eq ?_)
· rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
· simp [hf]
·
refine
(((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
(tendsto_id.prodMap (tendsto_fract_right _))).mono_right
(le_of_eq ?_) <;>
simp [nhdsWithin_prod_eq, nhdsWithin_univ]
· replace ht : t ≠ ⌊t⌋ := fun ht' => ht ⟨_, ht'⟩
refine (h.continuousAt ?_).comp (continuousAt_id.prodMap (continuousAt_fract ht))
exact prod_mem_nhds univ_mem (Icc_mem_nhds (fract_pos.2 ht) (fract_lt_one _))
