isCompact_preimage — Mathlib

English

If f has compact multiplicative support, f is continuous, K is closed and does not contain 1, then the preimage f⁻¹(K) is compact.

Русский

Если f имеет компактную мультиподдержку, f непрерывна, K замкнуто и не содержит 1, то предобраз f⁻¹(K) компактен.

LaTeX

$$$\\text{HasCompactMulSupport}(f) \\land \\text{Continuous}(f) \\land \\text{IsClosed}(K) \\land (1\\notin K) \\Rightarrow \\operatorname{IsCompact}(f^{-1}(K)).$$$

Lean4

@[to_additive]
theorem isCompact_preimage [TopologicalSpace β] {K : Set β} (h'f : HasCompactMulSupport f) (hf : Continuous f)
    (hk : IsClosed K) (h'k : 1 ∉ K) : IsCompact (f ⁻¹' K) :=
  by
  apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)
  apply subset_mulTSupport
  aesop

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