isOpen_inter_preimage

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#ContinuousOn.isOpen_inter_preimage

← MathLib Explorer

English

If f is continuous on s, and s and t are open, then s ∩ f^{-1}(t) is open.

Русский

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

LaTeX

$$$\\text{IsOpen}(s) \\to \\text{IsOpen}(t) \\to \\text{IsOpen}(s \\cap f^{-1}(t))$$$

Lean4

theorem isOpen_inter_preimage {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) (ht : IsOpen t) :
    IsOpen (s ∩ f ⁻¹' t) :=
  (continuousOn_open_iff hs).1 hf t ht

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru