empty_union

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.empty_union

← MathLib Explorer

English

The empty Finmap acts as a zero for union: ∅ ∪ s1 = s1.

Русский

Пустое множество действует как ноль для объединения: ∅ ∪ s1 = s1.

LaTeX

$$$ \emptyset \cup s_1 = s_1 $$$

Lean4

@[simp]
theorem empty_union {s₁ : Finmap β} : ∅ ∪ s₁ = s₁ :=
  induction_on s₁ fun s₁ => by
    rw [← empty_toFinmap]
    simp [-empty_toFinmap, union_toFinmap]

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

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

Разделы

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

Аффилиация

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