notMem_mulTSupport_iff_eventuallyEq

English

The topological support of the product f·g is contained in the union of the topological supports of f and g.

Русский

Топологическая опора произведения f·g ⊆ опора(f) ∪ опора(g).

LaTeX

$$$\operatorname{mulTSupport}(f) \cup \operatorname{mulTSupport}(g)$$$

Lean4

@[to_additive]
theorem notMem_mulTSupport_iff_eventuallyEq : x ∉ mulTSupport f ↔ f =ᶠ[𝓝 x] 1 := by
  simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop, ←
    disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]

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