coe_sInf

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Sublocale.coe_sInf

English

The underlying value of sInf s equals sInf of the image: (sInf s).val = sInf (Subtype.val '' s).

Русский

Значение подмножества sInf s равно инфимуму образа: (sInf s).val = sInf (Subtype.val '' s).

LaTeX

$$$(sInf s).\text{val} = \operatorname{sInf}(\operatorname{Subtype.val} \,' ' s)$$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (s : Set S) : (sInf s).val = sInf (Subtype.val '' s) :=
  rfl

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

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

Разделы

Аффилиация

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