isOpen_preimage — Mathlib

English

If f is ContinuousOn f s, s is open, and f^{-1}(t) ⊆ s with t open, then f^{-1}(t) is open.

Русский

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

LaTeX

$$$\\text{ContinuousOn } f s \\to \\text{IsOpen}(s) \\to f^{-1}(t) \\subseteq s \\to \\text{IsOpen}(t) \\Rightarrow \\text{IsOpen}(f^{-1}(t))$$$

Lean4

theorem isOpen_preimage {t : Set β} (h : ContinuousOn f s) (hs : IsOpen s) (hp : f ⁻¹' t ⊆ s) (ht : IsOpen t) :
    IsOpen (f ⁻¹' t) := by
  convert (continuousOn_open_iff hs).mp h t ht
  rw [inter_comm, inter_eq_self_of_subset_left hp]

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