Theorem IsClosed.exists_nat_bool_injection_of_not_countable

Modification history

2024-02-13 21:51
Mathlib/Topology/MetricSpace/Perfect.lean
refactor(Topology): split Topology.Perfect into two modules (#10272) …
Modified IsClosed.exists_nat_bool_injection_of_not_countableView on Github →
2023-08-10 19:52
Mathlib/Topology/Perfect.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified IsClosed.exists_nat_bool_injection_of_not_countableView on Github →
2023-04-27 21:26
Mathlib/Topology/Perfect.lean
chore: forward port leanprover-community/mathlib#18864 (#3687) …
Added IsClosed.exists_nat_bool_injection_of_not_countableView on Github →