forall_mem_not_eq'

Mathlib.Data.Finset.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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