forall_mem_not_eq

Mathlib.Data.Finset.Defs

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

English

(∀ b ∈ s, a ≠ b) iff a ∉ s.

Русский

Для всех b ∈ s, a ≠ b тогда и только тогда, когда a ∉ s.

LaTeX

$$$ (\forall b \in s, \neg a = b) \iff a \notin s $$$

Lean4

@[simp]
theorem forall_mem_not_eq {s : Finset α} {a : α} : (∀ b ∈ s, ¬a = b) ↔ a ∉ s := by aesop

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

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

Разделы

Аффилиация

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