coe_eq_univ

Mathlib.Order.BooleanSubalgebra

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

English

A subalgebra L equals univ if and only if L equals the top element ⊤.

Русский

Подалгебра L равна универсу, если и только если она равна вершине ⊤.

LaTeX

$$L = (univ : Set α) \iff L = ⊤$$

Lean4

@[simp, norm_cast]
theorem coe_eq_univ : L = (univ : Set α) ↔ L = ⊤ := by rw [← coe_top, coe_inj]

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

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

Разделы

Аффилиация

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