lowerSemicontinuous_iff_isClosed_preimage

English

Lower semicontinuity is equivalent to openness of preimages of all open rays Ioi(y).

Русский

Нижняя полупрерывность эквивалентна открытности прообразов всех лучей Ioi(y).

LaTeX

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

Lean4

theorem lowerSemicontinuous_iff_isClosed_preimage {f : α → γ} : LowerSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Iic y) :=
  by
  rw [lowerSemicontinuous_iff_isOpen_preimage]
  simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]

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