coe_inj

Mathlib.Order.BooleanSubalgebra

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

English

Atomistic property: for any a ≤ sSup S, there exists a subset of atoms representing a.

Русский

Свойство атомистичности: для любого a ≤ sSup S существует представление a как объединение атомов.

LaTeX

$$$ \forall a \le sSup S, \exists T \subseteq S, a = sSup T $$$

Lean4

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

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

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

Разделы

Аффилиация

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