Commit 2021-01-24 06:50 aa744dba

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.