exists_notMem

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.exists_notMem

English

There exists an embedding of the natural numbers into any infinite set s.

Русский

Существует вложение (инъекция) из \mathbb{N} в любую бесконечную подмножество s.

LaTeX

$$$ \exists i: \mathbb{N} \hookrightarrow s \quad \text{if } s \text{ is Infinite}$$$

Lean4

theorem exists_notMem (hs : s.Finite) : ∃ a, a ∉ s := by by_contra! h; exact infinite_univ (hs.subset fun a _ ↦ h _)

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

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

Разделы

Аффилиация

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