{"# Cardinality of the division ring generated by a set
Subfield.cardinalMk_closure_le_max: the cardinality of the (sub-)division ring
generated by a set is bounded by the cardinality of the set unless it is finite.
The method used to prove this (via WType) can be easily generalized to other algebraic
structures, but those cardinalities can usually be obtained by other means, using some
explicit universal objects.
"}
Subfield.cardinalMk_closure_le_max
theorem
: #(closure s) ≤ max #s ℵ₀
lemma cardinalMk_closure_le_max : #(closure s) ≤ max #s ℵ₀ :=
(Cardinal.mk_le_of_surjective <| surjective_ofWType s).trans <| by
convert WType.cardinalMk_le_max_aleph0_of_finite' using 1
· rw [lift_uzero, mk_sum, lift_uzero]
have : lift.{u,0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
obtain h|h := lt_or_le #s ℵ₀
· rw [max_eq_right h.le, max_eq_right]
exact (add_lt_aleph0 this h).le
· rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]
rintro (n|_)
· fin_cases n <;> (dsimp only [id_eq]; infer_instance)
infer_instanceSubfield.cardinalMk_closure
theorem
[Infinite s] : #(closure s) = #s
lemma cardinalMk_closure [Infinite s] : #(closure s) = #s :=
((cardinalMk_closure_le_max s).trans_eq <| max_eq_left <| aleph0_le_mk s).antisymm
(mk_le_mk_of_subset subset_closure)