union_toFinmap

Mathlib.Data.Finmap

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

English

The toFinmap map respects union: toFinmap s1 ∪ toFinmap s2 = toFinmap (s1 ∪ s2).

Русский

Функция toFinmap сохраняет объединение: toFinmap s1 ∪ toFinmap s2 = toFinmap (s1 ∪ s2).

LaTeX

$$$ (toFinmap\, s_1) \cup (toFinmap\, s_2) = toFinmap (s_1 \cup s_2) $$$

Lean4

@[simp]
theorem union_toFinmap (s₁ s₂ : AList β) : (toFinmap s₁) ∪ (toFinmap s₂) = toFinmap (s₁ ∪ s₂) := by
  simp [(· ∪ ·), union]

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

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

Разделы

Аффилиация

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