empty_iff

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordset.empty_iff

← MathLib Explorer

English

An Ordset is empty exactly when its underlying Ordnode is empty.

Русский

Пустой Ordset тогда и только тогда, когда его базовый Ordnode пуст.

LaTeX

$$$s = \\emptyset \\iff s.1.empty$$$

Lean4

theorem empty_iff {s : Ordset α} : s = ∅ ↔ s.1.empty :=
  ⟨fun h => by cases h; exact rfl, fun h => by
    cases s with
    | mk s_val _ => cases s_val <;> [rfl; cases h]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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