preimage

Mathlib.Topology.Continuous

URI: https://scilib.ai/kg/mathlib#IsOpen.preimage

English

If f is continuous, then the preimage of any open set is open.

Русский

Если f непрерывна, то прообраз любого открытого множества открыт.

LaTeX

$$$ (hf : \mathrm{Continuous}(f)) \rightarrow \forall t, \mathrm{IsOpen}(t) \rightarrow \mathrm{IsOpen}(f^{-1}(t)) $$$

Lean4

theorem preimage (hf : Continuous f) {t : Set Y} (h : IsOpen t) : IsOpen (f ⁻¹' t) :=
  hf.isOpen_preimage t h

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

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

Разделы

Аффилиация

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