English
If α is a proper space and f: α → β is expanding with respect to an onto map and continuous, then β is also proper.
Русский
Если пространство α — правильное, а отображение f: α → β расширяющее и сюрьективное, и непрерывное, то β тоже является правильным пространством.
LaTeX
$$$ \text{ProperSpace } \beta$ under $\text{ProperSpace } \alpha$, $\text{AntilipschitzWith } K f$, continuous surjection $f$$$
Lean4
/-- The image of a proper space under an expanding onto map is proper. -/
protected theorem properSpace {α : Type*} [MetricSpace α] {K : ℝ≥0} {f : α → β} [ProperSpace α]
(hK : AntilipschitzWith K f) (f_cont : Continuous f) (hf : Function.Surjective f) : ProperSpace β :=
by
refine ⟨fun x₀ r => ?_⟩
let K := f ⁻¹' closedBall x₀ r
have A : IsClosed K := isClosed_closedBall.preimage f_cont
have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall
have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
convert this.image f_cont
exact (hf.image_preimage _).symm
