exists_notMem_finset — Mathlib

English

If s is infinite and t is a Finset, there exists an element a with a ∈ s and a ∉ t.

Русский

Если s бесконечно, а t — конечно, существует элемент a, такой что a ∈ s и a ∉ t.

LaTeX

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

Lean4

theorem exists_notMem_finset (hs : s.Infinite) (t : Finset α) : ∃ a ∈ s, a ∉ t :=
  hs.exists_notMem_finite t.finite_toSet

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