mem_insert

Mathlib.Data.Finmap

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

English

a ∈ insert a' b' s iff a = a' or a ∈ s.

Русский

a принадлежит insert a' b' s тогда и только тогда, когда a = a' или a ∈ s.

LaTeX

$$$ a \in insert\ a' b' s \iff a = a' \lor a \in s $$$

Lean4

@[simp]
theorem mem_insert {a a' : α} {b' : β a'} {s : Finmap β} : a ∈ insert a' b' s ↔ a = a' ∨ a ∈ s :=
  induction_on s AList.mem_insert

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

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

Разделы

Аффилиация

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