English
Let α be a type, m,n ∈ ℕ, s ⊆ α. If s.ncard + n ≤ ENat.card α, then there exists y : Fin n ↪ α with Disjoint s and range y.
Русский
Пусть α — множество, m,n ∈ ℕ, s ⊆ α. Если s.ncard + n ≤ ENat.card α, существует вложение y: Fin n ↪ α с Disjoint(s, range(y)).
LaTeX
$$$s \\ncard + n \\le ENat.card \\alpha \\Rightarrow \\exists y : Fin(n) \\hookrightarrow \\alpha, \\operatorname{Disjoint}(s, \\operatorname{range}(y)).$$$
Lean4
theorem exists_embedding_disjoint_range_of_add_le_ENat_card [Finite s] (hs : s.ncard + n ≤ ENat.card α) :
∃ y : Fin n ↪ α, Disjoint s (range y) :=
by
rsuffices ⟨y⟩ : Nonempty (Fin n ↪ (sᶜ : Set α))
· use y.trans (subtype _)
rw [Set.disjoint_right]
rintro _ ⟨i, rfl⟩
simpa only [← mem_compl_iff] using Subtype.coe_prop (y i)
rcases finite_or_infinite α with hα | hα
· let _ : Fintype α := Fintype.ofFinite α
classical
apply nonempty_of_card_le
rwa [Fintype.card_fin, ← add_le_add_iff_left s.ncard, ← Nat.card_eq_fintype_card, Nat.card_coe_set_eq,
ncard_add_ncard_compl, ← ENat.coe_le_coe, ← ENat.card_eq_coe_natCard, ENat.coe_add]
· exact ⟨valEmbedding.trans s.toFinite.infinite_compl.to_subtype.natEmbedding⟩
