mulRothNumber_spec — Mathlib

English

There exists a witness t ⊆ s with #t = mulRothNumber s and ThreeGPFree t.

Русский

Существует подмножество t ⊆ s с кардинальностью #t = mulRothNumber s и ThreeGPFree t.

LaTeX

$$$\exists t\subseteq s\;\text{with}\;|t| = mulRothNumber(s) \land ThreeGPFree(t)$$$

Lean4

@[to_additive]
theorem mulRothNumber_spec : ∃ t ⊆ s, #t = mulRothNumber s ∧ ThreeGPFree (t : Set α) :=
  Nat.findGreatest_spec (P := fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (t : Set α)) (Nat.zero_le _)
    ⟨∅, empty_subset _, card_empty, by norm_cast; exact threeGPFree_empty⟩

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