continuous_isLeft

Mathlib.Topology.Constructions.SumProd

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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