Commit 2022-09-12 11:04 1c4e1843

refactor(set_theory/basic): match x < ℵ₀ lemmas with x ≤ ℵ₀ lemmas (#15662)

• Mark cardinal.lt_aleph_0_iff_set_finite as @[simp] lemma.
• Add cardinal.lt_aleph_0_iff_subtype_finite and cardinal.mk_le_aleph_0_iff; drop cardinal.encodable_iff.
• Rename cardinal.mk_set_le_aleph_0 to cardinal.le_aleph_0_iff_set_countable.
• Rename cardinal.mk_subtype_le_aleph_0 to cardinal.le_aleph_0_iff_subtype_countable.
• Make first_order.language.countable protected.
• Use [countable _] instead of [encodable _] or [nonempty (encodable _)] here and there.