continuousWithinAt_star

Mathlib.Topology.Algebra.Star

URI: https://scilib.ai/kg/mathlib#continuousWithinAt_star

English

The star map is continuous within any set at a point.

Русский

Операция звезды непрерывна внутри множества в точке.

LaTeX

$$$\forall s:\,\text{Set }R,\; \mathrm{ContinuousWithinAt}(\star, s, x)$$$

Lean4

theorem continuousWithinAt_star {s : Set R} {x : R} : ContinuousWithinAt star s x :=
  continuous_star.continuousWithinAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru