upperSemicontinuousWithinAt_univ_iff

English

Upper semicontinuity within the universal set is equivalent to ordinary upper semicontinuity.

Русский

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

LaTeX

$$$\\displaystyle \\text{UpperSemicontinuousWithinAt}(f,\\mathrm{univ},x) \\;\\Leftrightarrow \\; \\text{UpperSemicontinuousAt}(f,x)$$$

Lean4

theorem upperSemicontinuousWithinAt_univ_iff : UpperSemicontinuousWithinAt f univ x ↔ UpperSemicontinuousAt f x := by
  simp [UpperSemicontinuousWithinAt, UpperSemicontinuousAt, nhdsWithin_univ]

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