le_mk_iff_exists_subset — Mathlib

English

For any c, c ≤ |s| iff there exists a subset p ⊆ s with |p| = c.

Русский

Для любого c выполнено: c ≤ |s| тогда и только тогда, когда существует подмножество p ⊆ s такое, что |p| = c.

LaTeX

$$$c \\le |s| \\iff \\exists p \\subseteq s, |p| = c$$$

Lean4

theorem le_mk_iff_exists_subset {c : Cardinal} {α : Type u} {s : Set α} : c ≤ #s ↔ ∃ p : Set α, p ⊆ s ∧ #p = c :=
  by
  rw [le_mk_iff_exists_set, ← Subtype.exists_set_subtype]
  apply exists_congr; intro t; rw [mk_image_eq]; apply Subtype.val_injective

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