instSetLike

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.instSetLike

English

Sublattice α carries a canonical SetLike structure, identifying its carrier with the underlying set.

Русский

Sublattice α несёт каноническую структуру SetLike, связывая носитель с базовым множеством.

LaTeX

$$$\text{SetLike}(\text{Sublattice}(\alpha))$$$

Lean4

instance instSetLike : SetLike (Sublattice α) α
    where
  coe L := L.carrier
  coe_injective' L M h := by cases L; congr

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

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

Разделы

Аффилиация

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