Loogle!

Result

Found 306 declarations mentioning Dense. Of these, only the first 200 are shown.

• Dense 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] (s : Set X) : Prop
• BaireSpace.baire_property 📋 Mathlib.Topology.Defs.Basic
  {X : Type u_1} {inst✝ : TopologicalSpace X} [self : BaireSpace X] (f : ℕ → Set X) : (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
• BaireSpace.mk 📋 Mathlib.Topology.Defs.Basic
  {X : Type u_1} [TopologicalSpace X] (baire_property : ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)) : BaireSpace X
• dense_univ 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] : Dense Set.univ
• Dense.nonempty 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} [h : Nonempty X] (hs : Dense s) : s.Nonempty
• Dense.nonempty_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) : s.Nonempty ↔ Nonempty X
• Dense.closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s → Dense (closure s)
• Dense.of_closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense (closure s) → Dense s
• dense_closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense (closure s) ↔ Dense s
• Dense.closure_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s → closure s = Set.univ
• dense_iff_closure_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s ↔ closure s = Set.univ
• Dense.mono 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s₁ s₂ : Set X} (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂
• Dense.interior_compl 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : Dense s) : interior sᶜ = ∅
• interior_eq_empty_iff_dense_compl 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = ∅ ↔ Dense sᶜ
• Dense.inter_open_nonempty 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
• dense_iff_inter_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
• dense_compl_singleton_iff_not_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {x : X} : Dense {x}ᶜ ↔ ¬IsOpen {x}
• Dense.induction 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {P : X → Prop} (mem : ∀ x ∈ s, P x) (isClosed : IsClosed {x | P x}) (x : X) : P x
• Dense.exists_mem_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) : ∃ x ∈ s, x ∈ U
• Dense.inter_of_isOpen_left 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)
• Dense.inter_of_isOpen_right 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)
• Dense.open_subset_closure_inter 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s)
• Dense.inter_nhds_nonempty 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s t : Set X} (hs : Dense s) (ht : t ∈ nhds x) : (s ∩ t).Nonempty
• dense_compl_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense {x}ᶜ
• denseRange_subtype_val 📋 Mathlib.Topology.Continuous
  {X : Type u_1} [TopologicalSpace X] {p : X → Prop} : DenseRange Subtype.val ↔ Dense {x | p x}
• DenseRange.dense_image 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) : Dense (f '' s)
• Dense.denseRange_val 📋 Mathlib.Topology.Continuous
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : Dense s) : DenseRange Subtype.val
• Continuous.range_subset_closure_image_dense 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Continuous f) (hs : Dense s) : Set.range f ⊆ closure (f '' s)
• DenseRange.dense_of_mapsTo 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y} (ht : Set.MapsTo f s t) : Dense t
• dense_indiscrete 📋 Mathlib.Topology.Order
  {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] {s : Set α} (h : s.Nonempty) : Dense s
• dense_discrete 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {s : Set α} : Dense s ↔ s = Set.univ
• Dense.preimage 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (hs : Dense s) (hf : IsOpenMap f) : Dense (f ⁻¹' s)
• Topology.IsInducing.dense_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) {s : Set X} : Dense s ↔ ∀ (x : X), f x ∈ closure (f '' s)
• IsOpenQuotientMap.dense_preimage_iff 📋 Mathlib.Topology.Maps.OpenQuotient
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsOpenQuotientMap f) {s : Set Y} : Dense (f ⁻¹' s) ↔ Dense s
• Dense.prod 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : Dense s) (ht : Dense t) : Dense (s ×ˢ t)
• Dense.quotient 📋 Mathlib.Topology.Constructions
  {X : Type u} [Setoid X] [TopologicalSpace X] {s : Set X} (H : Dense s) : Dense (Quotient.mk' '' s)
• Subtype.dense_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set ↑s} : Dense t ↔ s ⊆ closure (Subtype.val '' t)
• exists_open_dense_of_open_dense_subtype 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {u : Set ↑s} (huo : IsOpen u) (hud : Dense u) : ∃ v, IsOpen v ∧ Dense v ∧ Subtype.val ⁻¹' v = u
• dense_pi 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → TopologicalSpace (α i)] {s : (i : ι) → Set (α i)} (I : Set ι) (hs : ∀ i ∈ I, Dense (s i)) : Dense (I.pi s)
• Dense.isSeparable_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set α} (hs : Dense s) : TopologicalSpace.IsSeparable s ↔ TopologicalSpace.SeparableSpace α
• TopologicalSpace.exists_countable_dense 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] : ∃ s, s.Countable ∧ Dense s
• TopologicalSpace.SeparableSpace.exists_countable_dense 📋 Mathlib.Topology.Bases
  {α : Type u} {t : TopologicalSpace α} [self : TopologicalSpace.SeparableSpace α] : ∃ s, s.Countable ∧ Dense s
• TopologicalSpace.SeparableSpace.mk 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] (exists_countable_dense : ∃ s, s.Countable ∧ Dense s) : TopologicalSpace.SeparableSpace α
• TopologicalSpace.separableSpace_iff 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] : TopologicalSpace.SeparableSpace α ↔ ∃ s, s.Countable ∧ Dense s
• TopologicalSpace.IsTopologicalBasis.dense_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {s : Set α} : Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
• Dense.exists_countable_dense_subset 📋 Mathlib.Topology.Bases
  {α : Type u_1} [TopologicalSpace α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t
• exists_countable_dense_bot_top 📋 Mathlib.Topology.Bases
  (α : Type u_1) [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [PartialOrder α] : ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
• Dense.exists_countable_dense_subset_bot_top 📋 Mathlib.Topology.Bases
  {α : Type u_1} [TopologicalSpace α] [PartialOrder α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
• Dense.diff_finite 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)
• Dense.sdiff_finite 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)
• Dense.diff_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : Dense s) (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense (s \ {x})
• Dense.sdiff_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : Dense s) (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense (s \ {x})
• Dense.diff_finset 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) (t : Finset X) : Dense (s \ ↑t)
• Dense.sdiff_finset 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) (t : Finset X) : Dense (s \ ↑t)
• IsOpen.dense 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} [TopologicalSpace X] {s : Set X} [PreirreducibleSpace X] (ho : IsOpen s) (hne : s.Nonempty) : Dense s
• preirreducibleSpace_iff_open_dense 📋 Mathlib.Topology.Irreducible
  (X : Type u_3) [TopologicalSpace X] : PreirreducibleSpace X ↔ ∀ ⦃U : Set X⦄, IsOpen U → U.Nonempty → Dense U
• Continuous.ext_on 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {s : Set Y} (hs : Dense s) {f g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : Set.EqOn f g s) : f = g
• Dense.orderDual 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) : Dense (⇑OrderDual.ofDual ⁻¹' s)
• Dense.exists_ge 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x ≤ y
• Dense.exists_gt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x < y
• Dense.exists_le 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y ≤ x
• Dense.exists_lt 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y < x
• Dense.exists_ge' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] {s : Set α} (hs : Dense s) (htop : ∀ (x : α), IsTop x → x ∈ s) (x : α) : ∃ y ∈ s, x ≤ y
• Dense.exists_le' 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] {s : Set α} (hs : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (x : α) : ∃ y ∈ s, y ≤ x
• Dense.exists_between 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) {x y : α} (h : x < y) : ∃ z ∈ s, z ∈ Set.Ioo x y
• Dense.Iio_eq_biUnion 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y
• Dense.Ioi_eq_biUnion 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) (x : α) : Set.Ioi x = ⋃ y ∈ s ∩ Set.Ioi x, Set.Ioi y
• Dense.extend 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : Dense s) (f : ↑s → β) : α → β
• IsDenseEmbedding.dense_image 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {e : α → β} (de : IsDenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ Dense s
• IsDenseInducing.dense_image 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} (di : IsDenseInducing i) {s : Set α} : Dense (i '' s) ↔ Dense s
• Dense.isDenseEmbedding_val 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseEmbedding Subtype.val
• Dense.isDenseInducing_val 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseInducing Subtype.val
• IsDenseInducing.interior_compact_eq_empty 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {i : α → β} [T2Space β] (di : IsDenseInducing i) (hd : Dense (Set.range i)ᶜ) {s : Set α} (hs : IsCompact s) : interior s = ∅
• Dense.comap_val_nhds_neBot 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : Dense s) (a : α) : (Filter.comap Subtype.val (nhds a)).NeBot
• Dense.extend_unique 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] {g : α → β} (hs : Dense s) (hf : ∀ (x : ↑s), g ↑x = f x) (hg : Continuous g) : hs.extend f = g
• Dense.extend_eq_of_tendsto 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] (hs : Dense s) {a : α} {b : β} (hf : Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) : hs.extend f a = b
• Dense.extend_eq 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] (hs : Dense s) (hf : Continuous f) (x : ↑s) : hs.extend f ↑x = f x
• Dense.continuous_extend 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] (hs : Dense s) (hf : ∀ (a : α), ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)) : Continuous (hs.extend f)
• Dense.extend_eq_at 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} [T2Space β] (hs : Dense s) {f : ↑s → β} {x : ↑s} (hf : ContinuousAt f x) : hs.extend f ↑x = f x
• Dense.continuousAt_extend 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T3Space β] {a : α} (hs : Dense s) (hf : ∀ᶠ (x : α) in nhds a, ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds x)) (nhds b)) : ContinuousAt (hs.extend f) a
• Dense.extend_unique_at 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : ↑s → β} [T2Space β] {a : α} {g : α → β} (hs : Dense s) (hf : ∀ᶠ (x : ↑s) in Filter.comap Subtype.val (nhds a), g ↑x = f x) (hg : ContinuousAt g a) : hs.extend f a = g a
• residual_of_dense_Gδ 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (ho : IsGδ s) (hd : Dense s) : s ∈ residual X
• residual_of_dense_open 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (ho : IsOpen s) (hd : Dense s) : s ∈ residual X
• isClosed_isNowhereDense_iff_compl 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ
• mem_residual_iff 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : s ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
• dense_of_mem_residual 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hs : s ∈ residual X) : Dense s
• not_isMeagre_of_isGδ_of_dense 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] [Nonempty X] {s : Set X} (hs : IsGδ s) (hd : Dense s) : ¬IsMeagre s
• dense_iInter_of_isOpen_nat 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {f : ℕ → Set X} (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)) : Dense (⋂ n, f n)
• IsGδ.baireSpace_of_dense 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hG : IsGδ s) (hd : Dense s) : BaireSpace ↑s
• dense_iInter_of_Gδ 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (ho : ∀ (s : ι), IsGδ (f s)) (hd : ∀ (s : ι), Dense (f s)) : Dense (⋂ s, f s)
• dense_iInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (ho : ∀ (i : ι), IsOpen (f i)) (hd : ∀ (i : ι), Dense (f i)) : Dense (⋂ s, f s)
• Dense.inter_of_Gδ 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) (hsc : Dense s) (htc : Dense t) : Dense (s ∩ t)
• dense_iUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : ⋃ i, f i = Set.univ) : Dense (⋃ i, interior (f i))
• mem_residual 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} : s ∈ residual X ↔ ∃ t ⊆ s, IsGδ t ∧ Dense t
• eventually_residual 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {p : X → Prop} : (∀ᶠ (x : X) in residual X, p x) ↔ ∃ t, IsGδ t ∧ Dense t ∧ ∀ x ∈ t, p x
• Set.Finite.dense_sInter 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] {s : Set (Set X)} (hs : s.Finite) (ho : ∀ t ∈ s, IsOpen t) (hd : ∀ t ∈ s, Dense t) : Dense (⋂₀ s)
• IsGδ.dense_iUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {s : Set X} (hs : IsGδ s) (hd : Dense s) {f : ι → Set X} (hc : ∀ (i : ι), IsClosed (f i)) (hU : s ⊆ ⋃ i, f i) : Dense (⋃ i, interior (f i))
• dense_sInter_of_Gδ 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsGδ s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)
• dense_sInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)
• dense_biInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (ho : ∀ s ∈ S, IsOpen (f s)) (hS : S.Countable) (hd : ∀ s ∈ S, Dense (f s)) : Dense (⋂ s ∈ S, f s)
• dense_sUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (hc : ∀ s ∈ S, IsClosed s) (hS : S.Countable) (hU : ⋃₀ S = Set.univ) : Dense (⋃ s ∈ S, interior s)
• dense_biInter_of_Gδ 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : (x : α) → x ∈ S → Set X} (ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)) (hS : S.Countable) (hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)) : Dense (⋂ s, ⋂ (h : s ∈ S), f s h)
• IsGδ.dense_sUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {T : Set (Set X)} {s : Set X} (hs : IsGδ s) (hd : Dense s) (hc : T.Countable) (hc' : ∀ t ∈ T, IsClosed t) (hU : s ⊆ ⋃₀ T) : Dense (⋃ t ∈ T, interior t)
• dense_biUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (hc : ∀ s ∈ S, IsClosed (f s)) (hS : S.Countable) (hU : ⋃ s ∈ S, f s = Set.univ) : Dense (⋃ s ∈ S, interior (f s))
• IsGδ.dense_biUnion_interior_of_closed 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {t : Set α} {s : Set X} (hs : IsGδ s) (hd : Dense s) (ht : t.Countable) {f : α → Set X} (hc : ∀ i ∈ t, IsClosed (f i)) (hU : s ⊆ ⋃ i ∈ t, f i) : Dense (⋃ i ∈ t, interior (f i))
• Dense.smul 📋 Mathlib.Topology.Algebra.ConstMulAction
  {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [Group G] [MulAction G α] [ContinuousConstSMul G α] (c : G) {s : Set α} (hs : Dense s) : Dense (c • s)
• Dense.vadd 📋 Mathlib.Topology.Algebra.ConstMulAction
  {α : Type u_2} {G : Type u_4} [TopologicalSpace α] [AddGroup G] [AddAction G α] [ContinuousConstVAdd G α] (c : G) {s : Set α} (hs : Dense s) : Dense (c +ᵥ s)
• ContinuousMap.injective_restrict 📋 Mathlib.Topology.ContinuousMap.Basic
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {s : Set α} (hs : Dense s) : Function.Injective (ContinuousMap.restrict s)
• Dense.biUnion_uniformity_ball 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : Set α} {U : SetRel α α} (hs : Dense s) (hU : U ∈ uniformity α) : ⋃ x ∈ s, UniformSpace.ball x U = Set.univ
• Dense.uniformContinuous_extend 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {s : Set α} {f : ↑s → β} [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) : UniformContinuous (hs.extend f)
• Dense.extend_of_ind 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {s : Set α} {f : ↑s → β} [T0Space β] (hs : Dense s) (hf : UniformContinuous f) (x : ↑s) : hs.extend f ↑x = f x
• Dense.extend_exists 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {s : Set α} {f : ↑s → β} [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) : ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)
• Dense.extend_spec 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {s : Set α} {f : ↑s → β} [CompleteSpace β] (hs : Dense s) (hf : UniformContinuous f) (a : α) : Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds (hs.extend f a))
• QuotientAddGroup.dense_preimage_mk 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} {s : Set (G ⧸ N)} : Dense (QuotientAddGroup.mk ⁻¹' s) ↔ Dense s
• QuotientGroup.dense_preimage_mk 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} {s : Set (G ⧸ N)} : Dense (QuotientGroup.mk ⁻¹' s) ↔ Dense s
• QuotientAddGroup.dense_image_mk 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G} {s : Set G} : Dense (QuotientAddGroup.mk '' s) ↔ Dense (s + ↑N)
• QuotientGroup.dense_image_mk 📋 Mathlib.Topology.Algebra.Group.Quotient
  {G : Type u_1} [TopologicalSpace G] [Group G] [SeparatelyContinuousMul G] {N : Subgroup G} {s : Set G} : Dense (QuotientGroup.mk '' s) ↔ Dense (s * ↑N)
• dense_of_exists_between 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α} (h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Set.Ioo a b) : Dense s
• Dense.topology_eq_generateFrom 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (hs : Dense s) : inst✝ = TopologicalSpace.generateFrom (Set.Ioi '' s ∪ Set.Iio '' s)
• dense_iff_exists_between 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} : Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b
• dense_coborder 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : Dense (coborder s)
• Submodule.dense_iff_topologicalClosure_eq_top 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] {s : Submodule R M} : Dense ↑s ↔ s.topologicalClosure = ⊤
• Submodule.isClosed_or_dense_of_isCoatom 📋 Mathlib.Topology.Algebra.Module.Basic
  {R : Type u} {M : Type v} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (s : Submodule R M) (hs : IsCoatom s) : IsClosed ↑s ∨ Dense ↑s
• ContinuousLinearMap.ext_on 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
  {R₁ : Type u_1} {R₂ : Type u_2} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [T2Space M₂] {s : Set M₁} (hs : Dense ↑(Submodule.span R₁ s)) {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• EMetric.dense_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [PseudoEMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.eball x r ∩ s).Nonempty
• Metric.dense_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.ball x r ∩ s).Nonempty
• Dense.exists_dist_lt 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ s, dist x y < ε
• Metric.dense_iff_iUnion_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, Metric.ball c r = Set.univ
• Dense.isGLB_inter_iff 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} : IsGLB (t ∩ s) x ↔ IsGLB t x
• Dense.isLUB_inter_iff 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {s t : Set α} (hs : Dense s) (ht : IsOpen t) {x : α} : IsLUB (t ∩ s) x ↔ IsLUB t x
• Dense.lowerBounds_image 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : lowerBounds (f '' S) = lowerBounds (Set.range f)
• Dense.upperBounds_image 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : upperBounds (f '' S) = upperBounds (Set.range f)
• Dense.ciInf' 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [ClosedIciTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : ⨅ s, f ↑s = ⨅ i, f i
• Dense.ciSup' 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) : ⨆ s, f ↑s = ⨆ i, f i
• Dense.ciInf 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLattice α] [ClosedIciTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) (h : BddBelow (Set.range f)) : ⨅ s, f ↑s = ⨅ i, f i
• Dense.ciSup 📋 Mathlib.Topology.Order.IsLUB
  {γ : Type u_2} {α : Type u_3} [TopologicalSpace α] [ConditionallyCompleteLattice α] [ClosedIicTopology α] {f : γ → α} [TopologicalSpace γ] {S : Set γ} (hS : Dense S) (hf : Continuous f) (h : BddAbove (Set.range f)) : ⨆ s, f ↑s = ⨆ i, f i
• Dense.exists_seq_strictAnti_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMaxOrder α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioi x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
• Dense.exists_seq_strictMono_tendsto 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [NoMinOrder α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) (x : α) : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Iio x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
• Dense.exists_seq_strictAnti_tendsto_of_lt 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) {x y : α} (hy : x < y) : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
• Dense.exists_seq_strictMono_tendsto_of_lt 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [FirstCountableTopology α] {s : Set α} (hs : Dense s) {x y : α} (hy : y < x) : ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
• exists_countable_dense_no_bot_top 📋 Mathlib.Topology.Order.DenselyOrdered
  (α : Type u_1) [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace.SeparableSpace α] [Nontrivial α] : ∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s
• Dense.exists_countable_dense_subset_no_bot_top 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
• AddSubgroup.dense_or_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) : Dense ↑S ∨ ∃ a, S = AddSubgroup.closure {a}
• Subgroup.dense_or_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) : Dense ↑S ∨ ∃ a, S = Subgroup.closure {a}
• AddSubgroup.dense_iff_ne_zmultiples 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] {s : AddSubgroup G} : Dense ↑s ↔ ∀ (a : G), s ≠ AddSubgroup.zmultiples a
• Subgroup.dense_iff_ne_zpowers 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] {s : Subgroup G} : Dense ↑s ↔ ∀ (a : G), s ≠ Subgroup.zpowers a
• AddSubgroup.dense_xor'_addCyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (s : AddSubgroup G) : Xor (Dense ↑s) (∃ a, s = AddSubgroup.zmultiples a)
• AddSubgroup.dense_xor_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (s : AddSubgroup G) : Xor (Dense ↑s) (∃ a, s = AddSubgroup.zmultiples a)
• Subgroup.dense_xor'_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G) : Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
• Subgroup.dense_xor_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] [Nontrivial G] [DenselyOrdered G] (s : Subgroup G) : Xor (Dense ↑s) (∃ a, s = Subgroup.zpowers a)
• AddSubgroup.dense_of_no_min 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hbot : S ≠ ⊥) (H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a) : Dense ↑S
• AddSubgroup.dense_of_not_isolated_zero 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [TopologicalSpace G] [OrderTopology G] [Archimedean G] (S : AddSubgroup G) (hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Set.Ioo 0 ε) : Dense ↑S
• Subgroup.dense_of_no_min 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hbot : S ≠ ⊥) (H : ¬∃ a, IsLeast {g | g ∈ S ∧ 1 < g} a) : Dense ↑S
• Subgroup.dense_of_not_isolated_one 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) (hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Set.Ioo 1 ε) : Dense ↑S
• continuous_prod_of_dense_continuous_lipschitzWith 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {s : Set α} (hs : Dense s) (ha : ∀ a ∈ s, Continuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)) : Continuous f
• continuous_prod_of_dense_continuous_lipschitzWith' 📋 Mathlib.Topology.EMetricSpace.Lipschitz
  {α : Type u} {β : Type v} {γ : Type w} [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {t : Set β} (ht : Dense t) (ha : ∀ (a : α), LipschitzWith K fun y => f (a, y)) (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f
• tendsto_of_no_upcrossings 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α} (hs : Dense s) (H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)) (h : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : ∃ c, Filter.Tendsto u f (nhds c)
• ENNReal.exists_countable_dense_no_zero_top 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  : ∃ s, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s
• Dense.lipschitzWith_extend 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace β] {s : Set α} (hs : Dense s) {f : ↑s → β} {K : NNReal} (hf : LipschitzWith K f) : LipschitzWith K (hs.extend f)
• ContinuousAlgHom.ext_on 📋 Mathlib.Topology.Algebra.Algebra
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] [T2Space B] {s : Set A} (hs : Dense ↑(Algebra.adjoin R s)) {f g : A →A[R] B} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• Dense.borel_eq_generateFrom_Icc_mem 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Set.Icc l u = S}
• Dense.borel_eq_generateFrom_Ico_mem 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMinOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
• Dense.borel_eq_generateFrom_Ioc_mem 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] [DenselyOrdered α] [NoMaxOrder α] {s : Set α} (hd : Dense s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
• Dense.borel_eq_generateFrom_Icc_mem_aux 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l ≤ u ∧ Set.Icc l u = S}
• Dense.borel_eq_generateFrom_Ico_mem_aux 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsBot x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → y ∈ s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
• Dense.borel_eq_generateFrom_Ioc_mem_aux 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_5} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SecondCountableTopology α] {s : Set α} (hd : Dense s) (hbot : ∀ (x : α), IsTop x → x ∈ s) (hIoo : ∀ (x y : α), x < y → Set.Ioo x y = ∅ → x ∈ s) : borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ioc l u = S}
• Metric.dense_iUnion_range_toInductiveLimit 📋 Mathlib.Topology.MetricSpace.Gluing
  {X : ℕ → Type u} [(n : ℕ) → MetricSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)} (I : ∀ (n : ℕ), Isometry (f n)) : Dense (⋃ i, Set.range (Metric.toInductiveLimit I i))
• MeasureTheory.Measure.dense_of_ae 📋 Mathlib.MeasureTheory.Measure.OpenPos
  {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {p : X → Prop} (hp : ∀ᵐ (x : X) ∂μ, p x) : Dense {x | p x}
• AddAction.dense_orbit 📋 Mathlib.Dynamics.Minimal
  (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] (x : α) : Dense (AddAction.orbit M x)
• MulAction.dense_orbit 📋 Mathlib.Dynamics.Minimal
  (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] (x : α) : Dense (MulAction.orbit M x)
• AddAction.IsMinimal.dense_orbit 📋 Mathlib.Dynamics.Minimal
  {M : Type u_1} {α : Type u_2} {inst✝ : AddMonoid M} {inst✝¹ : TopologicalSpace α} {inst✝² : AddAction M α} [self : AddAction.IsMinimal M α] (x : α) : Dense (AddAction.orbit M x)
• AddAction.IsMinimal.mk 📋 Mathlib.Dynamics.Minimal
  {M : Type u_1} {α : Type u_2} [AddMonoid M] [TopologicalSpace α] [AddAction M α] (dense_orbit : ∀ (x : α), Dense (AddAction.orbit M x)) : AddAction.IsMinimal M α
• MulAction.IsMinimal.dense_orbit 📋 Mathlib.Dynamics.Minimal
  {M : Type u_1} {α : Type u_2} {inst✝ : Monoid M} {inst✝¹ : TopologicalSpace α} {inst✝² : MulAction M α} [self : MulAction.IsMinimal M α] (x : α) : Dense (MulAction.orbit M x)
• MulAction.IsMinimal.mk 📋 Mathlib.Dynamics.Minimal
  {M : Type u_1} {α : Type u_2} [Monoid M] [TopologicalSpace α] [MulAction M α] (dense_orbit : ∀ (x : α), Dense (MulAction.orbit M x)) : MulAction.IsMinimal M α
• dense_of_nonempty_smul_invariant 📋 Mathlib.Dynamics.Minimal
  (M : Type u_1) {α : Type u_3} [Monoid M] [TopologicalSpace α] [MulAction M α] [MulAction.IsMinimal M α] {s : Set α} (hne : s.Nonempty) (hsmul : ∀ (c : M), c • s ⊆ s) : Dense s
• dense_of_nonempty_vadd_invariant 📋 Mathlib.Dynamics.Minimal
  (M : Type u_1) {α : Type u_3} [AddMonoid M] [TopologicalSpace α] [AddAction M α] [AddAction.IsMinimal M α] {s : Set α} (hne : s.Nonempty) (hvadd : ∀ (c : M), c +ᵥ s ⊆ s) : Dense s
• LinearMap.isClosed_or_dense_ker 📋 Mathlib.Topology.Algebra.Module.Simple
  {R : Type u} {M : Type v} {N : Type w} [Ring R] [TopologicalSpace R] [TopologicalSpace M] [AddCommGroup M] [AddCommGroup N] [Module R M] [ContinuousSMul R M] [Module R N] [ContinuousAdd M] [IsSimpleModule R N] (l : M →ₗ[R] N) : IsClosed ↑l.ker ∨ Dense ↑l.ker
• MeasureTheory.Lp.simpleFunc.dense 📋 Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
  {α : Type u_1} {E : Type u_4} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} [Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) : Dense ↑(MeasureTheory.Lp.simpleFunc E p μ)
• AddSubgroup.dense_of_infDist_le 📋 Mathlib.Analysis.Normed.Group.Lemmas
  {G : Type u_2} [SeminormedAddGroup G] (H : AddSubgroup G) (ε : ℝ) (h1 : 0 < ε) (h2 : ε < 1) (h : ∀ (g : G), Metric.infDist g ↑H ≤ ε * ‖g‖) : Dense ↑H
• Subgroup.dense_of_infDist_le 📋 Mathlib.Analysis.Normed.Group.Lemmas
  {G : Type u_2} [SeminormedGroup G] (H : Subgroup G) (ε : ℝ) (h1 : 0 < ε) (h2 : ε < 1) (h : ∀ (g : G), Metric.infDist g ↑H ≤ ε * ‖g‖) : Dense ↑H
• Dense.eq_of_inner_left 📋 Mathlib.Analysis.InnerProductSpace.Continuous
  {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 x v = inner 𝕜 y v) : x = y
• Dense.eq_of_inner_right 📋 Mathlib.Analysis.InnerProductSpace.Continuous
  {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 v x = inner 𝕜 v y) : x = y
• Dense.eq_zero_of_inner_left 📋 Mathlib.Analysis.InnerProductSpace.Continuous
  {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 x v = 0) : x = 0
• Dense.eq_zero_of_inner_right 📋 Mathlib.Analysis.InnerProductSpace.Continuous
  {E : Type u_3} (𝕜 : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {S : Set E} (hS : Dense S) (h : ∀ v ∈ S, inner 𝕜 v x = 0) : x = 0
• Dense.eq_of_sub_mem_orthogonal 📋 Mathlib.Analysis.InnerProductSpace.Projection.Submodule
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x y : E} (hK : Dense ↑K) (h : x - y ∈ Kᗮ) : x = y
• Dense.eq_zero_of_mem_orthogonal 📋 Mathlib.Analysis.InnerProductSpace.Projection.Submodule
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x : E} (hK : Dense ↑K) (h : x ∈ Kᗮ) : x = 0
• AlgebraicGeometry.Opens.isDominant_ι 📋 Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : Dense ↑U) : AlgebraicGeometry.IsDominant U.ι
• AlgebraicGeometry.Opens.isDominant_homOfLE 📋 Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : Dense ↑U) (hU' : U ≤ V) : AlgebraicGeometry.IsDominant (X.homOfLE hU')
• AlgebraicGeometry.ext_of_fromSpecResidueField_eq 📋 Mathlib.AlgebraicGeometry.Morphisms.Separated
  {X Y Z : AlgebraicGeometry.Scheme} (f g : X ⟶ Y) (i : Y ⟶ Z) [AlgebraicGeometry.IsSeparated i] [AlgebraicGeometry.IsReduced X] (S : Set ↥X) (hS' : Dense S) (H : ∀ x ∈ S, CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) f = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) g) (H' : CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i) : f = g
• AlgebraicGeometry.ext_of_apply_eq 📋 Mathlib.AlgebraicGeometry.AlgClosed.Basic
  {X Y : AlgebraicGeometry.Scheme} {K : Type u} [Field K] [IsAlgClosed K] {f g : X ⟶ Y} (i : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.IsSeparated i] [AlgebraicGeometry.LocallyOfFiniteType i] [AlgebraicGeometry.IsReduced X] [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f i)] (S : Set ↥X) (hS : IsLocallyClosed S) (hS' : Dense S) (H : ∀ x ∈ S, IsClosed {x} → f x = g x) (H' : CategoryTheory.CategoryStruct.comp f i = CategoryTheory.CategoryStruct.comp g i) : f = g
• AlgebraicGeometry.Scheme.PartialMap.dense_domain 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (self : X.PartialMap Y) : Dense ↑self.domain
• AlgebraicGeometry.Scheme.RationalMap.dense_domain 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) : Dense ↑f.domain
• AlgebraicGeometry.Scheme.PartialMap.mk 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (domain : X.Opens) (dense_domain : Dense ↑domain) (hom : ↑domain ⟶ Y) : X.PartialMap Y
• AlgebraicGeometry.Scheme.PartialMap.restrict 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : X.PartialMap Y
• AlgebraicGeometry.Scheme.PartialMap.restrict_equiv 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').equiv f
• AlgebraicGeometry.Scheme.PartialMap.restrict_domain 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').domain = U
• AlgebraicGeometry.Scheme.PartialMap.restrict_toRationalMap 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').toRationalMap = f.toRationalMap
• AlgebraicGeometry.Scheme.PartialMap.instIsOverRestrict 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y S : AlgebraicGeometry.Scheme} [X.Over S] [Y.Over S] (f : X.PartialMap Y) [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.restrict U hU hU')
• AlgebraicGeometry.Scheme.PartialMap.fromFunctionField_restrict 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) [IrreducibleSpace ↥X] {U : X.Opens} (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').fromFunctionField = f.fromFunctionField
• AlgebraicGeometry.Scheme.PartialMap.restrict_hom 📋 Mathlib.AlgebraicGeometry.Birational.RationalMap
  {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain) : (f.restrict U hU hU').hom = CategoryTheory.CategoryStruct.comp (X.homOfLE hU') f.hom

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59