lowerSemicontinuousWithinAt_univ_iff

English

Univ version equates LowerSemicontinuousWithinAt with LowerSemicontinuousAt.

Русский

Версия на Univ эквивалентна LowerSemicontinuousWithinAt и LowerSemicontinuousAt.

LaTeX

$$LowerSemicontinuousWithinAt f univ x ⇔ LowerSemicontinuousAt f x$$

Lean4

theorem lowerSemicontinuousWithinAt_univ_iff : LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x := by
  simp [LowerSemicontinuousWithinAt, LowerSemicontinuousAt, nhdsWithin_univ]

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