div_mem

Mathlib.Topology.UnitInterval

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

English

If x,y ∈ unitInterval with 0 ≤ x ≤ y, then x/y ∈ unitInterval.

Русский

Если x,y ∈ единичный интервал и 0 ≤ x ≤ y, то x/y ∈ единичный интервал.

LaTeX

$$$$ \forall x,y\in \text{unitInterval},\ 0\le x\le y \Rightarrow \frac{x}{y}\in \text{unitInterval}. $$$$

Lean4

theorem div_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) : x / y ∈ I :=
  ⟨div_nonneg hx hy, div_le_one_of_le₀ hxy hy⟩

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

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

Разделы

Аффилиация

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