mulTSupport_eq_empty_iff — Mathlib

English

The topological multiplicative support of f is empty if and only if f ≡ 1.

Русский

Топологическая поддержка умножения f пустая тогда и только тогда, когда f тождественно равна 1.

LaTeX

$$$\operatorname{mulTSupport}(f) = \emptyset \iff f = 1$$$

Lean4

@[to_additive]
theorem mulTSupport_eq_empty_iff {f : X → α} : mulTSupport f = ∅ ↔ f = 1 := by
  rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]

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