continuousOn_star

Mathlib.Topology.Algebra.Star

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

English

The star map is continuous on any set.

Русский

Операция звезды непрерывна на любом множестве.

LaTeX

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

Lean4

theorem continuousOn_star {s : Set R} : ContinuousOn star s :=
  continuous_star.continuousOn

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

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

Разделы

Аффилиация

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