continuous_qRight

Mathlib.Topology.Homotopy.HSpaces

URI: https://scilib.ai/kg/mathlib#unitInterval.continuous_qRight

← MathLib Explorer

English

The map qRight: I × I → I is continuous.

Русский

Карта qRight: I × I → I непрерывна.

LaTeX

$$$qRight\in C(I\times I, I)$$$

Lean4

@[fun_prop]
theorem continuous_qRight : Continuous qRight :=
  continuous_projIcc.comp <| Continuous.div (by fun_prop) (by fun_prop) fun _ ↦ (add_pos zero_lt_one).ne'

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

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

Разделы

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

Аффилиация

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