continuous_iff_lower_upperSemicontinuous

English

A function f is continuous iff it is simultaneously lower and upper semicontinuous.

Русский

Функция f непрерывна тогда и только тогда, когда она одновременно является нижнеполупрерывной и верхнеполупрерывной.

LaTeX

$$$$\\operatorname{Continuous} f \\iff \\operatorname{LowerSemicontinuous} f \\land \\operatorname{UpperSemicontinuous} f.$$$$

Lean4

theorem continuous_iff_lower_upperSemicontinuous {f : α → γ} :
    Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f := by
  simp_rw [← continuousOn_univ, continuousOn_iff_lower_upperSemicontinuousOn, lowerSemicontinuousOn_univ_iff,
    upperSemicontinuousOn_univ_iff]

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