English
If an infinite type β is covered by a union of Finsets f(a) (i.e., ⋃ a (f(a)) = ⊤), then the size of β is at most the size of the range of f.
Русский
Если бесконечный по мощности тип β покрывается объединением конечных множеств f(a), то мощность β не превосходит мощность множества образов f: β ≤ range f.
LaTeX
$$$#β \le #\mathrm{range}(f).$$$
Lean4
/-- If an infinite type `β` can be expressed as a union of finite sets,
then the cardinality of the collection of those finite sets
must be at least the cardinality of `β`. -/
-- TODO: write `Set.univ` instead of `⊤` and rename the theorem accordingly.
theorem le_range_of_union_finset_eq_top {α β : Type*} [Infinite β] (f : α → Finset β) (w : ⋃ a, (f a : Set β) = ⊤) :
#β ≤ #(range f) :=
by
have k : _root_.Infinite (range f) := by
rw [infinite_coe_iff]
apply mt (union_finset_finite_of_range_finite f)
rw [w]
exact infinite_univ
by_contra h
simp only [not_le] at h
let u : ∀ b, ∃ a, b ∈ f a := fun b => by simpa using (w.ge :) (Set.mem_univ b)
let u' : β → range f := fun b => ⟨f (u b).choose, by simp⟩
have v' : ∀ a, u' ⁻¹' {⟨f a, by simp⟩} ≤ f a := by
rintro a p m
have m : f (u p).choose = f a := by simpa [u'] using m
rw [← m]
apply fun b => (u b).choose_spec
obtain ⟨⟨-, ⟨a, rfl⟩⟩, p⟩ := exists_infinite_fiber u' h k
exact (@Infinite.of_injective _ _ p (inclusion (v' a)) (inclusion_injective _)).false
