exists_notMem — Mathlib

English

For an infinite α, every Finset t ⊆ α has an element a ∈ α with a ∉ t.

Русский

Для бесконечного α любой Finset t ⊆ α содержит элемент a ∈ α, который не принадлежит t.

LaTeX

$$$ [\text{Infinite}(\alpha)] \Rightarrow \forall t:\mathrm{Finset}(\alpha), \exists a \in \alpha, a \notin t $$$

Lean4

theorem _root_.Finset.exists_notMem (s : Finset α) : ∃ a, a ∉ s :=
  s.finite_toSet.exists_notMem

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