intro' — Mathlib

English

If K is compact and closed, and f equals 1 outside K, then HasCompactMulSupport f holds by a stronger condition.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem intro' (hK : IsCompact K) (h'K : IsClosed K) (hfK : ∀ x, x ∉ K → f x = 1) : HasCompactMulSupport f :=
  by
  have : mulTSupport f ⊆ K := by
    rw [← h'K.closure_eq]
    apply closure_mono (mulSupport_subset_iff'.2 hfK)
  exact IsCompact.of_isClosed_subset hK (isClosed_mulTSupport f) this

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