isOpen_preimage — Mathlib

English

A function f is lower semicontinuous if and only if for every y, the preimage of the open ray Ioi(y) is open.

Русский

Функция f нижняя полупрерывна тогда и только тогда, когда для каждого y прообраз открытого луча Ioi(y) открыт.

LaTeX

$$$\text{LowerSemicontinuous}(f) \iff \forall y, IsOpen (f^{-1}(Ioi(y)))$$$

Lean4

theorem isOpen_preimage (hf : LowerSemicontinuous f) (y : β) : IsOpen (f ⁻¹' Ioi y) :=
  lowerSemicontinuous_iff_isOpen_preimage.1 hf y

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