mathlib3

aa744dba - feat(topology/subset_properties): a locally compact space with second countable topology is sigma compact (#5689)

feat(topology/subset_properties): a locally compact space with second countable topology is sigma compact (#5689) * add `set.subsingleton.induction_on`, `set.Union_eq_univ_iff`, and `set.bUnion_eq_univ_iff`; * make `tactic.interactive.nontrivial` try `apply_instance` before `simp`; * add `dense.inter_nhds_nonempty`; * a subsingleton is compact (lemma for sets, instance for spaces); * in a locally compact space, every point has a compact neighborhood; * a compact space is sigma compact; * a locally compact space with second countable topology is sigma compact; * add `dense.bUnion_uniformity_ball`: the uniform neighborhoods of all points of a dense set cover the whole space Some of these changes are leftovers from a failed attempt to prove a wrong statement. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>