continuousAt_iff_lower_upperSemicontinuousAt

English

For a function f: α → γ into a linear order with order topology, continuity at x is equivalent to the conjunction of lower and upper semicontinuity at x.

Русский

Для функции f: α → γ в линейном порядке с топологией порядка, непрерывность в точке x эквивалентна сочетанию нижней и верхней полупрерывностей в x.

LaTeX

$$$$\\operatorname{ContinuousAt} f x \\iff \\operatorname{LowerSemicontinuousAt} f x \\land \\operatorname{UpperSemicontinuousAt} f x.$$$$

Lean4

theorem continuousAt_iff_lower_upperSemicontinuousAt {f : α → γ} :
    ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x := by
  simp_rw [← continuousWithinAt_univ, ← lowerSemicontinuousWithinAt_univ_iff, ← upperSemicontinuousWithinAt_univ_iff,
    continuousWithinAt_iff_lower_upperSemicontinuousWithinAt]

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