English
In general, if f has compact multiplicative support, then for any closed K not containing 1, the preimage f⁻¹(K) is compact.
Русский
Для любой закомпактированной мультиподдержки f и любого замкнутого K, не содержащего 1, предобраз f⁻¹(K) компактно.
LaTeX
$$$\\text{HasCompactMulSupport}(f) \\land \\text{Continuous}(f) \\land \\text{IsClosed}(K) \\land (1\\notin K) \\Rightarrow \\operatorname{IsCompact}(f^{-1}(K)).$$$
Lean4
/-- If `f` has compact multiplicative support, then `f` tends to 1 at infinity. -/
@[to_additive /-- If `f` has compact support, then `f` tends to zero at infinity. -/
]
theorem is_one_at_infty {f : α → γ} [TopologicalSpace γ] (h : HasCompactMulSupport f) : Tendsto f (cocompact α) (𝓝 1) :=
by
intro N hN
rw [mem_map, mem_cocompact']
refine ⟨mulTSupport f, h.isCompact, ?_⟩
rw [compl_subset_comm]
intro v hv
rw [mem_preimage, image_eq_one_of_notMem_mulTSupport hv]
exact mem_of_mem_nhds hN
