finite_mulSupport_of_discreteTopology

English

If α has the discrete topology and f: β → α is Multipliable, then the set { i ∈ β : f(i) ≠ 1 } is finite.

Русский

Если у α дискретная топология и f: β → α является Multipliable, тогда множество { i ∈ β : f(i) ≠ 1 } конечно.

LaTeX

$$$$\\{\,i\\in \\beta \\mid f(i) \\neq 1\\,\} \\text{ is finite}.$$$$

Lean4

@[to_additive]
theorem finite_mulSupport_of_discreteTopology {α : Type*} [CommGroup α] [TopologicalSpace α] [DiscreteTopology α]
    {β : Type*} (f : β → α) (h : Multipliable f) : Set.Finite f.mulSupport :=
  haveI : IsTopologicalGroup α := ⟨⟩
  h.tendsto_cofinite_one (discreteTopology_iff_singleton_mem_nhds.mp ‹_› 1)

Похожие утверждения