continuousOn_iff_lower_upperSemicontinuousOn

English

Continuity on a set s is equivalent to the conjunction of lower and upper semicontinuity on s.

Русский

Непрерывность на множества s равносильна сочетанию нижней и верхней полупрерывностей на s.

LaTeX

$$$$\\operatorname{ContinuousOn} f s \\iff \\operatorname{LowerSemicontinuousOn} f s \\land \\operatorname{UpperSemicontinuousOn} f s.$$$$

Lean4

theorem continuousOn_iff_lower_upperSemicontinuousOn {f : α → γ} :
    ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s :=
  by
  simp only [ContinuousOn, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]
  exact ⟨fun H => ⟨fun x hx => (H x hx).1, fun x hx => (H x hx).2⟩, fun H x hx => ⟨H.1 x hx, H.2 x hx⟩⟩

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