Loogle!

Result

Found 121 declarations mentioning TopologicalSpace.IsTopologicalBasis.

• TopologicalSpace.IsTopologicalBasis 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] (s : Set (Set α)) : Prop
• TopologicalSpace.isBasis_countableBasis 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : TopologicalSpace.IsTopologicalBasis (TopologicalSpace.countableBasis α)
• TopologicalSpace.isTopologicalBasis_opens 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis {U | IsOpen U}
• TopologicalSpace.isTopologicalBasis_empty 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis ∅ ↔ IsEmpty α
• TopologicalSpace.IsTopologicalBasis.eq_generateFrom 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (self : TopologicalSpace.IsTopologicalBasis s) : t = TopologicalSpace.generateFrom s
• TopologicalSpace.IsTopologicalBasis.secondCountableTopology 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α
• TopologicalSpace.IsTopologicalBasis.sUnion_eq 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (self : TopologicalSpace.IsTopologicalBasis s) : ⋃₀ s = Set.univ
• TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInter 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (hsg : t = TopologicalSpace.generateFrom s) (hsi : FiniteInter s) : TopologicalSpace.IsTopologicalBasis s
• TopologicalSpace.exists_seq_basis 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∃ b, TopologicalSpace.IsTopologicalBasis (Set.range b)
• TopologicalSpace.isTopologicalBasis_singleton_empty 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis {∅} ↔ IsEmpty α
• TopologicalSpace.IsTopologicalBasis.isOpen 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s
• isTopologicalBasis_singletons 📋 Mathlib.Topology.Bases
  (α : Type u_1) [TopologicalSpace α] [DiscreteTopology α] : TopologicalSpace.IsTopologicalBasis {s | ∃ x, s = {x}}
• TopologicalSpace.IsTopologicalBasis.insert_empty 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis s) : TopologicalSpace.IsTopologicalBasis (insert ∅ s)
• TopologicalSpace.IsTopologicalBasis.induced 📋 Mathlib.Topology.Bases
  {β : Type u_1} {α : Type u_2} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)} (h : TopologicalSpace.IsTopologicalBasis T) : TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
• IsOpenQuotientMap.isTopologicalBasis 📋 Mathlib.Topology.Bases
  {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {π : X → Y} (h : IsOpenQuotientMap π) {V : Set (Set X)} (hV : TopologicalSpace.IsTopologicalBasis V) : TopologicalSpace.IsTopologicalBasis (Set.image π '' V)
• TopologicalSpace.IsTopologicalBasis.isInducing 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] {f : α → β} {T : Set (Set β)} (hf : Topology.IsInducing f) (h : TopologicalSpace.IsTopologicalBasis T) : TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
• Topology.IsInducing.isTopologicalBasis 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsInducing f) {T : Set (Set β)} (h : TopologicalSpace.IsTopologicalBasis T) : TopologicalSpace.IsTopologicalBasis (Set.preimage f '' T)
• TopologicalSpace.IsTopologicalBasis.diff_empty 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis s) : TopologicalSpace.IsTopologicalBasis (s \ {∅})
• TopologicalSpace.IsTopologicalBasis.sdiff_empty 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis s) : TopologicalSpace.IsTopologicalBasis (s \ {∅})
• isTopologicalBasis_subtype 📋 Mathlib.Topology.Bases
  {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) : TopologicalSpace.IsTopologicalBasis (Set.preimage Subtype.val '' B)
• TopologicalSpace.exists_countable_basis 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
• TopologicalSpace.IsTopologicalBasis.exists_countable 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : TopologicalSpace.IsTopologicalBasis t✝) : ∃ s ⊆ t✝, s.Countable ∧ TopologicalSpace.IsTopologicalBasis s
• TopologicalSpace.IsTopologicalBasis.isQuotientMap 📋 Mathlib.Topology.Bases
  {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {π : X → Y} {V : Set (Set X)} (hV : TopologicalSpace.IsTopologicalBasis V) (h' : Topology.IsQuotientMap π) (h : IsOpenMap π) : TopologicalSpace.IsTopologicalBasis (Set.image π '' V)
• TopologicalSpace.IsTopologicalBasis.open_eq_sUnion 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S
• TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ 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
• TopologicalSpace.IsTopologicalBasis.finite_sUnion 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) : TopologicalSpace.IsTopologicalBasis (Set.sUnion '' {f | f.Finite ∧ f ⊆ B})
• TopologicalSpace.IsTopologicalBasis.continuous_iff 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] {B : Set (Set β)} (hB : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)
• TopologicalSpace.IsTopologicalBasis.isOpenMap_iff 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)
• TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : TopologicalSpace.IsTopologicalBasis s) (hss' : s ⊆ s') : TopologicalSpace.IsTopologicalBasis s'
• TopologicalSpace.IsTopologicalBasis.mem_nhds 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ nhds a
• TopologicalSpace.IsTopologicalBasis.nhds_hasBasis 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {a : α} : (nhds a).HasBasis (fun t => t ∈ b ∧ a ∈ t) fun t => t
• TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_nhds : ∀ (a : α), (nhds a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id) : TopologicalSpace.IsTopologicalBasis s
• TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
• TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis B) {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, v.Nonempty ∧ v ⊆ u
• TopologicalSpace.isTopologicalBasis_of_subbasis 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (hs : t = TopologicalSpace.generateFrom s) : TopologicalSpace.IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s})
• TopologicalSpace.IsTopologicalBasis.quotient 📋 Mathlib.Topology.Bases
  {X : Type u_1} [TopologicalSpace X] {S : Setoid X} {V : Set (Set X)} (hV : TopologicalSpace.IsTopologicalBasis V) (h : IsOpenMap Quotient.mk') : TopologicalSpace.IsTopologicalBasis (Set.image Quotient.mk' '' V)
• TopologicalSpace.IsTopologicalBasis.open_eq_iUnion 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ β f, u = ⋃ i, f i ∧ ∀ (i : β), f i ∈ B
• TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t✝ : Set α} (hB : TopologicalSpace.IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t✝) : s ⊆ t✝
• TopologicalSpace.IsTopologicalBasis.eq_of_forall_subset_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t✝ : Set α} (hB : TopologicalSpace.IsTopologicalBasis B) (hs : IsOpen s) (ht : IsOpen t✝) (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t✝) : s = t✝
• TopologicalSpace.IsTopologicalBasis.mem_closure_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {s : Set α} {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty
• TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u
• TopologicalSpace.IsTopologicalBasis.isOpen_induction 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {P : Set α → Prop} (hB : TopologicalSpace.IsTopologicalBasis B) (basis : ∀ b ∈ B, P b) (sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)) {s : Set α} (hs : IsOpen s) : P s
• TopologicalSpace.IsTopologicalBasis.prod 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => x1 ×ˢ x2) B₁ B₂)
• TopologicalSpace.IsTopologicalBasis.isOpen_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) : IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s
• TopologicalSpace.IsTopologicalBasis.mem_nhds_iff 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) : s ∈ nhds a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
• TopologicalSpace.IsTopologicalBasis.inf 📋 Mathlib.Topology.Bases
  {β : Type u_1} {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)} (h₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => x1 ∩ x2) B₁ B₂)
• TopologicalSpace.IsTopologicalBasis.continuousOn_iff 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] {s : Set α} [TopologicalSpace β] {B : Set (Set β)} (hB : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : ContinuousOn f s ↔ ∀ t_1 ∈ B, ∃ u, IsOpen u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
• TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {r : Set (Set α)} (hsg : t = TopologicalSpace.generateFrom r) (hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r) : TopologicalSpace.IsTopologicalBasis (insert Set.univ r)
• TopologicalSpace.IsTopologicalBasis.sigma 📋 Mathlib.Topology.Bases
  {ι : Type u_1} {E : ι → Type u_2} [(i : ι) → TopologicalSpace (E i)] {s : (i : ι) → Set (Set (E i))} (hs : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (s i)) : TopologicalSpace.IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)
• TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : TopologicalSpace.IsTopologicalBasis s
• TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : TopologicalSpace.IsTopologicalBasis t✝) {u : Set α} (hu : IsOpen u) : ∃ s ⊆ t✝, s.Countable ∧ u = ⋃ a ∈ s, a
• TopologicalSpace.IsTopologicalBasis.sum 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] {s : Set (Set α)} (hs : TopologicalSpace.IsTopologicalBasis s) {t✝ : Set (Set β)} (ht : TopologicalSpace.IsTopologicalBasis t✝) : TopologicalSpace.IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t✝)
• TopologicalSpace.IsTopologicalBasis.inf_induced 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] {γ : Type u_2} [s : TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) (f₁ : γ → α) (f₂ : γ → β) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun x1 x2 => f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)
• TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B B' : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) (h_open : ∀ u ∈ B', IsOpen u) (h : ∀ u ∈ B, ∀ x ∈ u, ∃ v ∈ B', x ∈ v ∧ v ⊆ u) : TopologicalSpace.IsTopologicalBasis B'
• TopologicalSpace.IsTopologicalBasis.exists_subset_inter 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (self : TopologicalSpace.IsTopologicalBasis s) (t₁ : Set α) : t₁ ∈ s → ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
• isTopologicalBasis_pi 📋 Mathlib.Topology.Bases
  {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {T : (i : ι) → Set (Set (X i))} (cond : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) : TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}
• TopologicalSpace.isTopologicalBasis_of_cover 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} {U : ι → Set α} (Uo : ∀ (i : ι), IsOpen (U i)) (Uc : ⋃ i, U i = Set.univ) {b : (i : ι) → Set (Set ↑(U i))} (hb : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (b i)) : TopologicalSpace.IsTopologicalBasis (⋃ i, Set.image Subtype.val '' b i)
• TopologicalSpace.IsTopologicalBasis.mk 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (exists_subset_inter : ∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂) (sUnion_eq : ⋃₀ s = Set.univ) (eq_generateFrom : t = TopologicalSpace.generateFrom s) : TopologicalSpace.IsTopologicalBasis s
• IsTopologicalBasis.iInf 📋 Mathlib.Topology.Bases
  {β : Type u_1} {ι : Type u_2} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)} (h_basis : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) : TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}
• IsTopologicalBasis.iInf_induced 📋 Mathlib.Topology.Bases
  {β : Type u_1} {ι : Type u_2} {X : ι → Type u_3} [t : (i : ι) → TopologicalSpace (X i)] {T : (i : ι) → Set (Set (X i))} (cond : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) (f : (i : ι) → β → X i) : TopologicalSpace.IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}
• TopologicalSpace.IsTopologicalBasis.inseparable_iff 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x y : X} : Inseparable x y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
• TopologicalSpace.IsTopologicalBasis.eq_iff 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T0Space X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x y : X} : x = y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s
• TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x y : X} (h : x ≠ y) : ∃ a ∈ b, x ∈ a ∧ y ∉ a
• TopologicalSpace.IsTopologicalBasis.isOpen_isPreconnected 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] [LocallyConnectedSpace α] : TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
• locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} [TopologicalSpace α] : LocallyConnectedSpace α ↔ TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
• isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsLindelof (b i)) (U : Set X) : IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
• TopologicalSpace.IsTopologicalBasis.nhds_basis_closure 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) (x : X) : (nhds x).HasBasis (fun s => x ∈ s ∧ s ∈ B) closure
• TopologicalSpace.IsTopologicalBasis.open_eq_sUnion_of_closure_subset 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {U : Set X} (hU : IsOpen U) : U = ⋃₀ {v | v ∈ B ∧ closure v ⊆ U}
• TopologicalSpace.IsTopologicalBasis.exists_closure_subset 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ nhds x) : ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s
• TopologicalSpace.IsTopologicalBasis.open_eq_sUnion_closure 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {U : Set X} (hU : IsOpen U) : U = ⋃₀ {v | ∃ u ∈ B, closure u ⊆ U ∧ v = closure u}
• TopologicalSpace.IsTopologicalBasis.open_eq_iUnion_of_closure_subset 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {U : Set X} (hU : IsOpen U) : U = ⋃ v ∈ B, ⋃ (_ : closure v ⊆ U), v
• TopologicalSpace.IsTopologicalBasis.open_eq_iUnion_closure 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {U : Set X} (hU : IsOpen U) : U = ⋃ v ∈ B, ⋃ (_ : closure v ⊆ U), closure v
• isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [ts : TopologicalSpace α] [Preorder α] (c : Set α) (h : ts = TopologicalSpace.generateFrom {s | ∃ a ∈ c, s = Set.Ioi a ∨ s = Set.Iio a}) : TopologicalSpace.IsTopologicalBasis {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Set.Ioi a) ∩ ⋂ a ∈ g, Set.Iio a}
• eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open 📋 Mathlib.Topology.Compactness.Bases
  {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) : ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
• isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis 📋 Mathlib.Topology.Compactness.Bases
  {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set X) : IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
• eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open 📋 Mathlib.Topology.Compactness.Bases
  {X : Type u_1} [TopologicalSpace X] (b : Set (Set X)) (hb : TopologicalSpace.IsTopologicalBasis b) (U : Set X) (hUc : IsCompact U) (hUo : IsOpen U) : ∃ s, U = ⋃₀ (Subtype.val '' ↑s)
• TopologicalSpace.IsOpenCover.isTopologicalBasis 📋 Mathlib.Topology.Sets.OpenCover
  {ι : Type u_1} {X : Type u_3} [TopologicalSpace X] {u : ι → TopologicalSpace.Opens X} (hu : TopologicalSpace.IsOpenCover u) {B : (i : ι) → Set (Set ↥(u i))} (hB : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (B i)) : TopologicalSpace.IsTopologicalBasis (⋃ i, (fun x => Subtype.val '' x) '' B i)
• QuasiSeparatedSpace.of_isTopologicalBasis 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {b : ι → Set α} (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_inter : ∀ (i j : ι), IsCompact (b i ∩ b j)) : QuasiSeparatedSpace α
• PrespectralSpace.isTopologicalBasis 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : PrespectralSpace X] : TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}
• PrespectralSpace.mk 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_3} [TopologicalSpace X] (isTopologicalBasis : TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}) : PrespectralSpace X
• prespectralSpace_iff 📋 Mathlib.Topology.Spectral.Prespectral
  (X : Type u_3) [TopologicalSpace X] : PrespectralSpace X ↔ TopologicalSpace.IsTopologicalBasis {U | IsOpen U ∧ IsCompact U}
• PrespectralSpace.of_isTopologicalBasis' 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {b : ι → Set X} (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_basis : ∀ (i : ι), IsCompact (b i)) : PrespectralSpace X
• PrespectralSpace.of_isTopologicalBasis 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_1} [TopologicalSpace X] {B : Set (Set X)} (basis : TopologicalSpace.IsTopologicalBasis B) (isCompact_basis : ∀ U ∈ B, IsCompact U) : PrespectralSpace X
• Topology.IsConstructible.induction_of_isTopologicalBasis 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] [CompactSpace X] {P : (s : Set X) → Topology.IsConstructible s → Prop} [QuasiSeparatedSpace X] {ι : Type u_4} [Nonempty ι] (b : ι → Set X) (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_basis : ∀ (i : ι), IsCompact (b i)) (sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯) (union : ∀ (s : Set X) (hs : Topology.IsConstructible s) (t : Set X) (ht : Topology.IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯) (s : Set X) (hs : Topology.IsConstructible s) : P s hs
• PrimeSpectrum.isTopologicalBasis_basic_opens 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] : TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(PrimeSpectrum.basicOpen r))
• MeasureTheory.Measure.isTopologicalBasis_isOpen_lt_top 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {m0 : MeasurableSpace α} [TopologicalSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] : TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ μ s < ⊤}
• TopologicalSpace.IsTopologicalBasis.borel_eq_generateFrom 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] {s : Set (Set α)} (hs : TopologicalSpace.IsTopologicalBasis s) : borel α = MeasurableSpace.generateFrom s
• Real.isTopologicalBasis_Ioo_rat 📋 Mathlib.Topology.Instances.Real.Lemmas
  : TopologicalSpace.IsTopologicalBasis (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
• PiNat.isTopologicalBasis_cylinders 📋 Mathlib.Topology.MetricSpace.PiNat
  (E : ℕ → Type u_1) [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] : TopologicalSpace.IsTopologicalBasis {s | ∃ x n, s = PiNat.cylinder x n}
• AlgebraicGeometry.Scheme.affineBasisCover_is_basis 📋 Mathlib.AlgebraicGeometry.Cover.Open
  (X : AlgebraicGeometry.Scheme) : TopologicalSpace.IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
• ProjectiveSpectrum.isTopologicalBasis_basic_opens 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
  {A : Type u_1} {σ : Type u_2} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] : TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(ProjectiveSpectrum.basicOpen 𝒜 r))
• TopologicalSpace.vietoris.isTopologicalBasis 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis ((fun u => {s | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen U})
• TopologicalSpace.IsTopologicalBasis.compacts 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) : TopologicalSpace.IsTopologicalBasis ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u ⊆ B})
• TopologicalSpace.Compacts.isTopologicalBasis 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ ∀ U ∈ u, IsOpen U})
• TopologicalSpace.IsTopologicalBasis.nonemptyCompacts 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) : TopologicalSpace.IsTopologicalBasis ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
• TopologicalSpace.NonemptyCompacts.isTopologicalBasis 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] : TopologicalSpace.IsTopologicalBasis ((fun u => {K | ↑K ⊆ ⋃₀ u ∧ ∀ U ∈ u, (↑K ∩ U).Nonempty}) '' {u | u.Finite ∧ u.Nonempty ∧ ∀ U ∈ u, IsOpen U})
• TopologicalSpace.IsTopologicalBasis.vietoris 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) : TopologicalSpace.IsTopologicalBasis ((fun p => {s | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) '' {p | IsOpen p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
• IsLocalHomeomorph.isTopologicalBasis 📋 Mathlib.Topology.IsLocalHomeomorph
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsLocalHomeomorph f) : TopologicalSpace.IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}
• ultrafilterBasis_is_basis 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)
• totallySeparatedSpace_of_t0_of_basis_clopen 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_1} [TopologicalSpace X] [T0Space X] (h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}) : TotallySeparatedSpace X
• isTopologicalBasis_isClopen 📋 Mathlib.Topology.Separation.Profinite
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• loc_compact_Haus_tot_disc_of_zero_dim 📋 Mathlib.Topology.Separation.Profinite
  {H : Type u_2} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• TopCat.isTopologicalBasis_cofiltered_limit 📋 Mathlib.Topology.Category.TopCat.Limits.Cofiltered
  {J : Type v} [CategoryTheory.Category.{w, v} J] [CategoryTheory.IsCofiltered J] (F : CategoryTheory.Functor J TopCat) (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C) (T : (j : J) → Set (Set ↑(F.obj j))) (hT : ∀ (j : J), TopologicalSpace.IsTopologicalBasis (T j)) (univ : ∀ (i : J), Set.univ ∈ T i) (inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i) (compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i) : TopologicalSpace.IsTopologicalBasis {U | ∃ j, ∃ V ∈ T j, U = ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) ⁻¹' V}
• Ctop.toTopsp_isTopologicalBasis 📋 Mathlib.Data.Analysis.Topology
  {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) : TopologicalSpace.IsTopologicalBasis (Set.range F.f)
• Ctop.Realizer.is_basis 📋 Mathlib.Data.Analysis.Topology
  {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) : TopologicalSpace.IsTopologicalBasis (Set.range F.F.f)
• ContinuousMap.compactOpen_eq_generateFrom 📋 Mathlib.Topology.ContinuousMap.SecondCountableSpace
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set (Set X)} {T : Set (Set Y)} (hS₁ : ∀ K ∈ S, IsCompact K) (hT : TopologicalSpace.IsTopologicalBasis T) (hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) : ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 (fun K t => {f | Set.MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T})
• CompletelyRegularSpace.of_isTopologicalBasis_clopens 📋 Mathlib.Topology.Separation.CompletelyRegular
  {X : Type u} [TopologicalSpace X] (h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}) : CompletelyRegularSpace X
• CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum 📋 Mathlib.Topology.Separation.CompletelyRegular
  {X : Type u} [TopologicalSpace X] [CompletelyRegularSpace X] (hX : Cardinal.mk X < Cardinal.continuum) : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• CompleteType.isTopologicalBasis_range_typesWith 📋 Mathlib.ModelTheory.Topology.Types
  {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1} : TopologicalSpace.IsTopologicalBasis (Set.range T.typesWith)
• Filter.isTopologicalBasis_Iic_principal 📋 Mathlib.Topology.Filter
  {α : Type u_2} : TopologicalSpace.IsTopologicalBasis (Set.range (Set.Iic ∘ Filter.principal))
• Topology.IsLower.isTopologicalBasis 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : TopologicalSpace.IsTopologicalBasis (Topology.IsLower.lowerBasis α)
• Topology.IsUpper.isTopologicalBasis 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : TopologicalSpace.IsTopologicalBasis (Topology.IsUpper.upperBasis α)
• Topology.IsLower.isTopologicalBasis_insert_univ_subbasis 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [Topology.IsLower α] : TopologicalSpace.IsTopologicalBasis (insert Set.univ {s | ∃ a, (Set.Ici a)ᶜ = s})
• Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [Topology.IsUpper α] : TopologicalSpace.IsTopologicalBasis (insert Set.univ {s | ∃ a, (Set.Iic a)ᶜ = s})
• PrimitiveSpectrum.isTopologicalBasis_relativeLower 📋 Mathlib.Topology.Order.HullKernel
  {α : Type u_1} [SemilatticeInf α] {T : Set α} [OrderTop α] [TopologicalSpace α] [Topology.IsLower α] (hT : ∀ p ∈ T, InfPrime p) : TopologicalSpace.IsTopologicalBasis {S | ∃ a, (PrimitiveSpectrum.hull T a)ᶜ = S}
• Topology.IsLawson.isTopologicalBasis 📋 Mathlib.Topology.Order.LawsonTopology
  (α : Type u_1) [Preorder α] [TopologicalSpace α] [Topology.IsLawson α] : TopologicalSpace.IsTopologicalBasis (Topology.IsLawson.lawsonBasis α)
• HasSmallInductiveDimensionLT_one_iff 📋 Mathlib.Topology.SmallInductiveDimension
  {X : Type u_1} [TopologicalSpace X] : HasSmallInductiveDimensionLT X 1 ↔ TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• hasSmallInductiveDimensionLT_one_iff 📋 Mathlib.Topology.SmallInductiveDimension
  {X : Type u_1} [TopologicalSpace X] : HasSmallInductiveDimensionLT X 1 ↔ TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
• HasSmallInductiveDimensionLT.succ 📋 Mathlib.Topology.SmallInductiveDimension
  {X : Type u} [TopologicalSpace X] (n : ℕ) (s : Set (Set X)) (hs : TopologicalSpace.IsTopologicalBasis s) (h : ∀ U ∈ s, HasSmallInductiveDimensionLT (↑(frontier U)) n) : HasSmallInductiveDimensionLT X (n + 1)
• TopologicalSpace.isTopologicalBasis_clopens 📋 Mathlib.Topology.UniformSpace.Ultra.Basic
  {X : Type u_1} [UniformSpace X] [IsUltraUniformity X] : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}

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 ce5dd8c