isClosed_preimage — Mathlib

English

If f is lower semicontinuous, then the preimage of every lower closed ray Iic y is closed.

Русский

Если f — нижняя полупрерывная, то прообраз каждого замкнутого луча Iic(y) замкнут.

LaTeX

$$$\text{LowerSemicontinuous}(f) \Rightarrow \forall y, IsClosed (f^{-1}(Iic(y)))$$$

Lean4

theorem isClosed_preimage {f : α → γ} (hf : LowerSemicontinuous f) (y : γ) : IsClosed (f ⁻¹' Iic y) :=
  lowerSemicontinuous_iff_isClosed_preimage.1 hf y

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