locallyFinite_mulSupport_iff — Mathlib

English

Locally finite of multiplicative supports is equivalent to local finiteness of multiplicative support sets.

Русский

Локальная конечность множеств опор умножения эквивалентна локальной конечности соответствующих множеств опор.

LaTeX

$$$\operatorname{LocallyFinite}\bigl(i\mapsto \operatorname{mulSupport}(f_i)\bigr) \iff \operatorname{LocallyFinite}\bigl(i\mapsto \operatorname{mulTSupport}(f_i)\bigr}.$$$

Lean4

@[to_additive]
theorem locallyFinite_mulSupport_iff [One M] {f : ι → X → M} :
    (LocallyFinite fun i ↦ mulSupport <| f i) ↔ LocallyFinite fun i ↦ mulTSupport <| f i :=
  ⟨LocallyFinite.closure, fun H ↦ H.subset fun _ ↦ subset_closure⟩

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