exists_notMem_finite — Mathlib

English

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

Русский

Пусть s бесконечно, t конечно. Тогда существует элемент a, принадлежащий s, но не принадлежащий t.

LaTeX

$$$ s\ \text{Infinite} \land t\ \text{Finite} \Rightarrow \exists a\,(a \in s \land a \notin t) $$$

Lean4

theorem exists_notMem_finite (hs : s.Infinite) (ht : t.Finite) : ∃ a, a ∈ s ∧ a ∉ t := by by_contra! h;
  exact hs <| ht.subset h

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