exists_superset_card_eq — Mathlib

English

If s is a finite subset of α, and card constraints hold, there exists a superset t with s ⊆ t and |t| = n.

Русский

Если s — множество подмножеств α и выполняются ограничение по кардиналу, существует супермножество t с s ⊆ t и |t| = n.

LaTeX

$$$[Fintype\\;\\alpha] \\;\\{n: \\mathbb{N}\\}\\; (|s| \\le n) (n \\le |\\alpha|) \\Rightarrow \\exists t,\\ s \\subseteq t \\wedge |t| = n.$$$

Lean4

/-- We can inflate a set `s` to any bigger size. -/
theorem exists_superset_card_eq [Fintype α] {n : ℕ} {s : Finset α} (hsn : #s ≤ n) (hnα : n ≤ Fintype.card α) :
    ∃ t, s ⊆ t ∧ #t = n := by simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα

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