coe_Iio

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.coe_Iio

English

The finset Iio(a) corresponds to the set { x ∈ α | x < a }.

Русский

Финсет Iio(a) соответствует множеству { x ∈ α | x < a }.

LaTeX

$$$(Iio\,a \colon \mathrm{Set}\ \alpha) = \{ x \in \alpha \mid x < a \}$$$

Lean4

@[simp, norm_cast]
theorem coe_Iio (a : α) : (Iio a : Set α) = Set.Iio a :=
  Set.ext fun _ => mem_Iio

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

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

Разделы

Аффилиация

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