From 6c1ea0d78a74032ba8d6419c6669bae716af2c04 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 16 Aug 2023 05:50:37 +0000 Subject: [PATCH] chore(Topology/Bases): minor golf (#6584) --- Mathlib/Topology/Bases.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index ef5d87dc4b611..d5bb0cef988d7 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -230,11 +230,10 @@ theorem IsTopologicalBasis.isOpenMap_iff {β} [TopologicalSpace β] {B : Set (Se #align topological_space.is_topological_basis.is_open_map_iff TopologicalSpace.IsTopologicalBasis.isOpenMap_iff theorem IsTopologicalBasis.exists_nonempty_subset {B : Set (Set α)} (hb : IsTopologicalBasis B) - {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u := by - cases' hu with x hx - rw [hb.open_eq_sUnion' ou, mem_sUnion] at hx - rcases hx with ⟨v, hv, hxv⟩ - exact ⟨v, hv.1, ⟨x, hxv⟩, hv.2⟩ + {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u := + let ⟨x, hx⟩ := hu + let ⟨v, vB, xv, vu⟩ := hb.exists_subset_of_mem_open hx ou + ⟨v, vB, ⟨x, xv⟩, vu⟩ #align topological_space.is_topological_basis.exists_nonempty_subset TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset theorem isTopologicalBasis_opens : IsTopologicalBasis { U : Set α | IsOpen U } :=