mem_erase

Mathlib.Data.Finmap

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

English

a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s.

Русский

a' принадлежит erase a s тогда и только тогда, когда a' ≠ a и a' принадлежит s.

LaTeX

$$$ a' \in erase\ a\ s \iff a' \neq a \wedge a' \in s. $$$

Lean4

@[simp]
theorem mem_erase {a a' : α} {s : Finmap β} : a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s :=
  induction_on s fun s => by simp

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

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

Разделы

Аффилиация

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