coe_inj

Mathlib.Order.Sublattice

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

English

Two Sublattices are equal iff their underlying carrier sets are equal.

Русский

Два подслойства равны тогда и только тогда, когда их носители равны.

LaTeX

$$$(L : Set \alpha) = (M : Set \alpha) \iff L = M$$$

Lean4

theorem coe_inj : (L : Set α) = M ↔ L = M :=
  SetLike.coe_set_eq

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

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

Разделы

Аффилиация

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