continuous_isRight

Mathlib.Topology.Constructions.SumProd

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

← MathLib Explorer

English

The map isRight: X ⊕ Y → Bool is continuous.

Русский

Функция isRight: X ⊕ Y → Bool непрерывна.

LaTeX

$$$\\\\operatorname{Continuous}(\\\\mathrm{isRight})$$$

Lean4

@[continuity, fun_prop]
theorem continuous_isRight : Continuous (isRight : X ⊕ Y → Bool) :=
  continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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