union_empty

Mathlib.Data.Finmap

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

← MathLib Explorer

English

Union with the empty Finmap on the right leaves the left unchanged: s1 ∪ ∅ = s1.

Русский

Объединение с пустым справа не меняет левую часть: s1 ∪ ∅ = s1.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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