Theorems · Theorem · logic and foundations

Set.to_countable

∀ {α : Type u} (s : Set α) [Countable ↑s], s.Countable

Prove Set.Countable from a Countable instance on the subtype.

Defined in

Mathlib.Data.Set.Countable

Cited by

46 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Countable