preimage_isClosed_of_isClosed — Mathlib

English

If f is ContinuousOn f s, s is closed, and t is closed, then s ∩ f^{-1}(t) is closed.

Русский

Если f непрерывна на s, s и t замкнуты, то s ∩ f^{-1}(t) замкнуто.

LaTeX

$$$\\text{ContinuousOn } f s \\land \\text{IsClosed } s \\land \\text{IsClosed } t \\Rightarrow \\text{IsClosed } (s \\cap f^{-1}(t))$$$

Lean4

theorem preimage_isClosed_of_isClosed {t : Set β} (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) :
    IsClosed (s ∩ f ⁻¹' t) := by
  rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩
  rw [inter_comm, hu.2]
  apply IsClosed.inter hu.1 hs

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