erase_ne_self

Mathlib.Data.Finset.Erase

URI: https://scilib.ai/kg/mathlib#Finset.erase_ne_self

English

erase s a is not equal to s exactly when a ∈ s.

Русский

erase s a ≠ s тогда и только тогда, когда a ∈ s.

LaTeX

$$$ \mathrm{erase}(s,a) \neq s \iff a \in s $$$

Lean4

theorem erase_ne_self : s.erase a ≠ s ↔ a ∈ s :=
  erase_eq_self.not_left

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

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

Разделы

Аффилиация

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