exists_compact_iff_hasCompactMulSupport

English

There exists a compact K outside which f equals 1 if and only if HasCompactMulSupport f.

Русский

Существование компактного K таково, что вне K f = 1 тогда и только тогда, когда HasCompactMulSupport f.

LaTeX

$$$\exists K\; IsCompact(K) \land \forall x, x \notin K \to f(x)=1 \quad\iff\quad HasCompactMulSupport(f)$$$

Lean4

@[to_additive]
theorem exists_compact_iff_hasCompactMulSupport [R1Space α] :
    (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f := by
  simp_rw [← notMem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl, hasCompactMulSupport_def,
    exists_isCompact_superset_iff]

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