intro — Mathlib

English

If K is compact and f equals 1 outside K, then HasCompactMulSupport f holds.

Русский

Если K компактно и f(x)=1 за пределами K, то HasCompactMulSupport f выполняется.

LaTeX

$$$IsCompact(K) \Rightarrow (\forall x, x \notin K \to f(x)=1) \Rightarrow HasCompactMulSupport(f)$$$

Lean4

@[to_additive]
theorem intro [R1Space α] (hK : IsCompact K) (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f :=
  exists_compact_iff_hasCompactMulSupport.mp ⟨K, hK, hfK⟩

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