ne_of_mem_erase

Mathlib.Data.Finset.Erase

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

English

If b ∈ erase s a, then b ≠ a.

Русский

Если b принадлежит erase s a, то b ≠ a.

LaTeX

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

Lean4

theorem ne_of_mem_erase : b ∈ erase s a → b ≠ a := fun h => (mem_erase.1 h).1

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

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

Разделы

Аффилиация

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