instZeroLEOneClass

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Icc.instZeroLEOneClass

English

The interval Icc(0,1) is equipped with a structure that encodes 0 ≤ x ≤ 1 for all x in the interval.

Русский

Интервал Icc(0,1) снабжается структурой, в которой для любого элемента x выполняются неравенства 0 ≤ x ≤ 1.

LaTeX

$$$\forall x \in Icc(0,1),\ 0 \le x \le 1$$$

Lean4

instance instZeroLEOneClass : ZeroLEOneClass (Icc (0 : R) 1) :=
  ⟨Subtype.coe_le_coe.mp zero_le_one⟩

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

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

Разделы

Аффилиация

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