English
For an infinite index set β and a Hausdorff topological group G, a constant a yields Multipliable (fun _ : β ↦ a) iff a = 1.
Русский
Для бесконечного множества индексов β и пространства группы G, константа a дает Multipliable (функцию, которая постоянно принимает значение a) тогда и только тогда, когда a = 1.
LaTeX
$$$$\text{Multipliable} (\lambda _ : \beta, a) \iff a = 1.$$$$
Lean4
@[to_additive]
theorem multipliable_const_iff [Infinite β] [T2Space G] (a : G) : Multipliable (fun _ : β ↦ a) ↔ a = 1 :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· by_contra ha
have : { a }ᶜ ∈ 𝓝 1 := compl_singleton_mem_nhds (Ne.symm ha)
have : Finite β := by simpa [← Set.finite_univ_iff] using h.tendsto_cofinite_one this
exact not_finite β
· rintro rfl
exact multipliable_one
