instMul

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ioo.instMul

← MathLib Explorer

English

The product of two elements of Ioo(0,1) is again in Ioo(0,1).

Русский

Произведение двух элементов Ioo(0,1) снова лежит в Ioo(0,1).

LaTeX

$$$\forall p,q \in (0,1),\ 0 < p q < 1$$$

Lean4

instance instMul : Mul (Ioo (0 : R) 1) where
  mul p q := ⟨p.1 * q.1, ⟨mul_pos p.2.1 q.2.1, mul_lt_one_of_nonneg_of_lt_one_right p.2.2.le q.2.1.le q.2.2⟩⟩

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

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

Разделы

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

Аффилиация

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