coe_unitIntervalSubmonoid — Mathlib

English

The submonoid structure on the unit interval coincides with the unit interval itself as a subset of the reals.

Русский

Структура подмонойды на единичном интервале совпадает с самим единичным интервалом как подмножество вещественных чисел.

LaTeX

$$unitInterval.submonoid = unitInterval$$

Lean4

@[simp]
theorem coe_unitIntervalSubmonoid : submonoid = unitInterval :=
  rfl

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