isOpen_mulSupport — Mathlib

English

A continuous function has open support in the sense of the product topology; more precisely, mulSupport of a continuous map is open in the target.

Русский

непрерывная функция имеет открытое множество опоры в рамках произведения; конкретно mulSupport непрерывной функции открыто в области значений.

LaTeX

$$$\\text{Continuous}(f) \\Rightarrow IsOpen(\\mathrm{mulSupport}(f))$$$

Lean4

@[to_additive]
theorem isOpen_mulSupport [T1Space X] [One X] [TopologicalSpace Y] {f : Y → X} (hf : Continuous f) :
    IsOpen (mulSupport f) :=
  isOpen_ne.preimage hf

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