mul_mem

Mathlib.Topology.UnitInterval

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

English

If x,y ∈ unitInterval, then x·y ∈ unitInterval.

Русский

Если x,y ∈ единичный интервал, то произведение x·y также принадлежит единичному интервалу.

LaTeX

$$$$ \forall x,y\in \text{unitInterval},\; x\cdot y \in \text{unitInterval}. $$$$

Lean4

theorem mul_mem {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : x * y ∈ I :=
  ⟨mul_nonneg hx.1 hy.1, mul_le_one₀ hx.2 hy.1 hy.2⟩

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

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

Разделы

Аффилиация

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