From 69adfea7ea6eacb83097ff8c868ce81c807baf1b Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 14 Mar 2024 06:52:08 +0000 Subject: [PATCH] chore(Topology/Instances/Discrete): merge 2 instances (#11296) Prove `DiscreteTopology.secondCountableTopology_of_countable` directly, deprecate `DiscreteTopology.secondCountableTopology_of_encodable`. --- Mathlib/Topology/Instances/Discrete.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Instances/Discrete.lean b/Mathlib/Topology/Instances/Discrete.lean index 10a5352c87f58..a8e0ecbf5d4a7 100644 --- a/Mathlib/Topology/Instances/Discrete.lean +++ b/Mathlib/Topology/Instances/Discrete.lean @@ -33,18 +33,19 @@ instance (priority := 100) DiscreteTopology.firstCountableTopology [DiscreteTopo nhds_generated_countable := by rw [nhds_discrete]; exact isCountablyGenerated_pure #align discrete_topology.first_countable_topology DiscreteTopology.firstCountableTopology -instance (priority := 100) DiscreteTopology.secondCountableTopology_of_encodable - [hd : DiscreteTopology α] [Encodable α] : SecondCountableTopology α := +instance (priority := 100) DiscreteTopology.secondCountableTopology_of_countable + [hd : DiscreteTopology α] [Countable α] : SecondCountableTopology α := haveI : ∀ i : α, SecondCountableTopology (↥({i} : Set α)) := fun i => { is_open_generated_countable := ⟨{univ}, countable_singleton _, by simp only [eq_iff_true_of_subsingleton]⟩ } secondCountableTopology_of_countable_cover (singletons_open_iff_discrete.mpr hd) (iUnion_of_singleton α) -#align discrete_topology.second_countable_topology_of_encodable DiscreteTopology.secondCountableTopology_of_encodable +#align discrete_topology.second_countable_topology_of_encodable DiscreteTopology.secondCountableTopology_of_countable -instance (priority := 100) DiscreteTopology.secondCountableTopology_of_countable {α : Type*} +@[deprecated DiscreteTopology.secondCountableTopology_of_countable] -- 2024-03-11 +theorem DiscreteTopology.secondCountableTopology_of_encodable {α : Type*} [TopologicalSpace α] [DiscreteTopology α] [Countable α] : SecondCountableTopology α := - @DiscreteTopology.secondCountableTopology_of_encodable _ _ _ (Encodable.ofCountable _) + DiscreteTopology.secondCountableTopology_of_countable #align discrete_topology.second_countable_topology_of_countable DiscreteTopology.secondCountableTopology_of_countable theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder [PartialOrder α] [PredOrder α]