English
The topological support of f is the closure of its support: the closure of the set where f(x) ≠ 1 (multiplicative setting).
Русский
Топологическая опора функции f есть замыкание её опоры: замыкание множества точек, где f(x) ≠ 1.
LaTeX
$$$\operatorname{mulTSupport}(f) = \overline{\operatorname{mulSupport}(f)}$$$
Lean4
/-- The topological support of a function is the closure of its support, i.e. the closure of the
set of all elements where the function is not equal to 1. -/
@[to_additive /-- The topological support of a function is the closure of its support. i.e. the
closure of the set of all elements where the function is nonzero. -/
]
def mulTSupport (f : X → α) : Set X :=
closure (mulSupport f)
