exists_notMem_finset

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Infinite.exists_notMem_finset

English

For any infinite α and any Finset s ⊆ α, there exists x ∈ α \ s.

Русский

Для любой бесконечной α и любого конечного подмножества s ⊆ α существует x ∈ α \ s.

LaTeX

$$[Infinite α] (s: Finset α) → ∃ x, x ∉ s$$

Lean4

theorem exists_notMem_finset [Infinite α] (s : Finset α) : ∃ x, x ∉ s :=
  not_forall.1 fun h => Fintype.false ⟨s, h⟩

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

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

Разделы

Аффилиация

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