upperSemicontinuousOn_univ_iff — Mathlib

English

Upper semicontinuity on the universal set is equivalent to standard upper semicontinuity.

Русский

Верхняя полупрерывность на универсовом множестве эквивалентна обычной верхней полупрерывности.

LaTeX

$$$\\displaystyle \\text{UpperSemicontinuousOn}(f,\\mathrm{univ}) \\Leftrightarrow \\text{UpperSemicontinuous}(f)$$$

Lean4

theorem upperSemicontinuousOn_univ_iff : UpperSemicontinuousOn f univ ↔ UpperSemicontinuous f := by
  simp [UpperSemicontinuousOn, UpperSemicontinuous, upperSemicontinuousWithinAt_univ_iff]

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