exists_nat_subset_range — Mathlib

English

For any finite s ⊆ ℕ, there exists n with s ⊆ range(n).

Русский

Для любого конечного множества s ⊆ ℕ существует n, такое что s ⊆ range(n).

LaTeX

$$$$ \forall s:\text{Finset}\,\mathbb{N}, \exists n:\mathbb{N}, s \subseteq \operatorname{range}(n). $$$$

Lean4

theorem exists_nat_subset_range (s : Finset ℕ) : ∃ n : ℕ, s ⊆ range n :=
  s.induction_on (by simp) fun a _ _ ⟨n, hn⟩ => ⟨max (a + 1) n, by grind⟩

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