upperClosure_eq_top_iff

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#upperClosure_eq_top_iff

English

A simple equivalence: upperClosure s = ⊤ iff s = ∅.

Русский

Простое равенство: верхнее замыкание s равно ⊤ тогда и только тогда, когда s пусто.

LaTeX

$$$upperClosure(s) = \top \iff s = \varnothing$$$

Lean4

@[simp]
theorem upperClosure_eq_top_iff : upperClosure s = ⊤ ↔ s = ∅ :=
  (@gc_upperClosure_coe α _).l_eq_bot.trans subset_empty_iff

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

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

Разделы

Аффилиация

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