exists_subset_card_eq — Mathlib

English

Same as above: If s ⊆ t and #s ≤ n ≤ #t, there exists u with s ⊆ u ⊆ t and |u| = n.

Русский

То же самое: если s ⊆ t и #s ≤ n ≤ #t, существует u с s ⊆ u ⊆ t и |u| = n.

LaTeX

$$$s \\subseteq t \\land #s \\le n \\land n \\le #t \\Rightarrow \\exists u, s \\subseteq u \\land u \\subseteq t \\land #u = n$$$

Lean4

/-- We can shrink a set to any smaller size. -/
theorem exists_subset_card_eq (hns : n ≤ #s) : ∃ t ⊆ s, #t = n := by
  simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

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