mem_unitIntervalSubmonoid

Mathlib.Topology.UnitInterval

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

English

For any real x, x is in the submonoid iff x ∈ [0,1].

Русский

Для любого x ∈ \mathbb{R}, x принадлежит подмонойду тогда и только тогда, когда x ∈ [0,1].

LaTeX

$$∀x ∈ ℝ, x ∈ [0,1] ⇔ x ∈ unitInterval$$

Lean4

@[simp]
theorem mem_unitIntervalSubmonoid {x} : x ∈ submonoid ↔ x ∈ unitInterval :=
  Iff.rfl

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

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

Разделы

Аффилиация

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