English
Another formulation of the scalar-tower compatibility for ZeroAtInftyContinuousMap.
Русский
Ещё одно формулирование совместимости скалярного тTower для ZeroAtInftyContinuousMap.
LaTeX
$$IsScalarTower R (ZeroAtInftyContinuousMap α β) (ZeroAtInftyContinuousMap α β).$$
Lean4
protected theorem bounded (f : F) : ∃ C, ∀ x y : α, dist ((f : α → β) x) (f y) ≤ C :=
by
obtain ⟨K : Set α, hK₁, hK₂⟩ :=
mem_cocompact.mp (tendsto_def.mp (zero_at_infty (f : F)) _ (closedBall_mem_nhds (0 : β) zero_lt_one))
obtain ⟨C, hC⟩ := (hK₁.image (map_continuous f)).isBounded.subset_closedBall (0 : β)
refine ⟨max C 1 + max C 1, fun x y => ?_⟩
have : ∀ x, f x ∈ closedBall (0 : β) (max C 1) := by
intro x
by_cases hx : x ∈ K
· exact (mem_closedBall.mp <| hC ⟨x, hx, rfl⟩).trans (le_max_left _ _)
· exact (mem_closedBall.mp <| mem_preimage.mp (hK₂ hx)).trans (le_max_right _ _)
exact (dist_triangle (f x) 0 (f y)).trans (add_le_add (mem_closedBall.mp <| this x) (mem_closedBall'.mp <| this y))
