Loogle!

Result

Found 157 declarations mentioning Specializes.

• Specializes 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} [TopologicalSpace X] (x y : X) : Prop
• specializes_refl 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] (x : X) : x ⤳ x
• specializes_rfl 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x : X} : x ⤳ x
• specializes_of_eq 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (e : x = y) : x ⤳ y
• Specializes.of_eq 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (e : x = y) : x ⤳ y
• Inseparable.specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (h : Inseparable x y) : x ⤳ y
• Inseparable.specializes' 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (h : Inseparable x y) : y ⤳ x
• specializes_iff_clusterPt 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ ClusterPt y (pure x)
• Specializes.antisymm 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (h₁ : x ⤳ y) (h₂ : y ⤳ x) : Inseparable x y
• ker_nhds_eq_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x : X} : (nhds x).ker = {y | y ⤳ x}
• Specializes.trans 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y z : X} : x ⤳ y → y ⤳ z → x ⤳ z
• inseparable_iff_specializes_and 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : Inseparable x y ↔ x ⤳ y ∧ y ⤳ x
• Specializes.clusterPt 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {f : Filter X} (h : x ⤳ y) (hx : ClusterPt x f) : ClusterPt y f
• Specializes.mem_closure 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y → y ∈ closure {x}
• specializes_iff_mem_closure 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ y ∈ closure {x}
• Specializes.map 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hf : Continuous f) : f x ⤳ f y
• Specializes.map_of_continuousAt 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {f : X → Y} (h : x ⤳ y) (hf : ContinuousAt f y) : f x ⤳ f y
• Specializes.nhds_le_nhds 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y → nhds x ≤ nhds y
• Topology.IsInducing.specializes_iff 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {f : X → Y} (hf : Topology.IsInducing f) : f x ⤳ f y ↔ x ⤳ y
• specializes_iff_nhds 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ nhds x ≤ nhds y
• Specializes.pure_le_nhds 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y → pure x ≤ nhds y
• specializes_iff_pure 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ pure x ≤ nhds y
• Specializes.mem_closed 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (h : x ⤳ y) (hs : IsClosed s) (hx : x ∈ s) : y ∈ s
• Specializes.mem_open 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) : x ∈ s
• specializes_iff_forall_closed 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
• specializes_iff_forall_open 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
• subtype_specializes_iff 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {p : X → Prop} (x y : Subtype p) : x ⤳ y ↔ ↑x ⤳ ↑y
• specializes_pi 📋 Mathlib.Topology.Inseparable
  {ι : Type u_5} {A : ι → Type u_6} [(i : ι) → TopologicalSpace (A i)] {f g : (i : ι) → A i} : f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
• IsClosed.not_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ⤳ y
• IsOpen.not_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (hs : IsOpen s) (hx : x ∉ s) (hy : y ∈ s) : ¬x ⤳ y
• Specializes.fst 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a b : X × Y} (h : a ⤳ b) : a.1 ⤳ b.1
• Specializes.snd 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a b : X × Y} (h : a ⤳ b) : a.2 ⤳ b.2
• Specializes.closure_subset 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y → closure {y} ⊆ closure {x}
• specializes_iff_closure_subset 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ closure {y} ⊆ closure {x}
• Tendsto.specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {f g : X → Y} {l : Filter X} {y : Y} (h : Filter.Tendsto g l (nhds y)) (hl : ∀ (x : X), f x ⤳ g x) : Filter.Tendsto f l (nhds y)
• Filter.HasBasis.specializes_iff 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set X} (h : (nhds y).HasBasis p s) : x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i
• Specializes.prod 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) : (x₁, y₁) ⤳ (x₂, y₂)
• not_specializes_iff_exists_closed 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : ¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
• not_specializes_iff_exists_open 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} : ¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
• Specializes.map_of_continuousWithinAt 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {f : X → Y} {s : Set X} (h : x ⤳ y) (hf : ContinuousWithinAt f s y) (hx : x ∈ s) : f x ⤳ f y
• Specializes.not_disjoint 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} (h : x ⤳ y) : ¬Disjoint (nhds x) (nhds y)
• specializes_of_nhdsWithin 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (h₁ : nhdsWithin x s ≤ nhdsWithin y s) (h₂ : x ∈ s) : x ⤳ y
• specializes_prod 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x₁ x₂ : X} {y₁ y₂ : Y} : (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
• Specializes.map_of_continuousOn 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x y : X} {f : X → Y} {s : Set X} (h : x ⤳ y) (hf : ContinuousOn f s) (hx : x ∈ s) (hy : y ∈ s) : f x ⤳ f y
• IsCompact.of_subset_of_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hs : IsCompact s) (hts : t ⊆ s) (h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y) : IsCompact t
• IsClosed.continuous_piecewise_of_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f g : X → Y} [DecidablePred fun x => x ∈ s] (hs : IsClosed s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ (x : X), g x ⤳ f x) : Continuous (s.piecewise f g)
• IsOpen.continuous_piecewise_of_specializes 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f g : X → Y} [DecidablePred fun x => x ∈ s] (hs : IsOpen s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ (x : X), f x ⤳ g x) : Continuous (s.piecewise f g)
• specializes_TFAE 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] (x y : X) : [x ⤳ y, pure x ≤ nhds y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s, y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE
• R0Space.mk 📋 Mathlib.Topology.Separation.Basic
  {X : Type u} [TopologicalSpace X] (specializes_symm : Std.Symm Specializes) : R0Space X
• R0Space.specializes_symm 📋 Mathlib.Topology.Separation.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} [self : R0Space X] : Std.Symm Specializes
• R0Space.specializes_symmetric 📋 Mathlib.Topology.Separation.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} [self : R0Space X] : Std.Symm Specializes
• r0Space_iff 📋 Mathlib.Topology.Separation.Basic
  (X : Type u) [TopologicalSpace X] : R0Space X ↔ Std.Symm Specializes
• Specializes.eq 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ⤳ y) : x = y
• specializes_iff_eq 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} : x ⤳ y ↔ x = y
• t1Space_iff_specializes_imp_eq 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
• Specializes.inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y → Inseparable x y
• Specializes.symm 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} (h : x ⤳ y) : y ⤳ x
• specializes_comm 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y ↔ y ⤳ x
• specializes_eq_eq 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] : (fun x1 x2 => x1 ⤳ x2) = Eq
• specializes_iff_inseparable 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R0Space X] {x y : X} : x ⤳ y ↔ Inseparable x y
• isClosed_setOfPred_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | p.1 ⤳ p.2}
• isClosed_setOf_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p | p.1 ⤳ p.2}
• R1Space.of_continuous_specializes_imp 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hc : Continuous f) (hspec : ∀ (x y : Y), f x ⤳ f y → x ⤳ y) : R1Space Y
• R1Space.mk 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} [TopologicalSpace X] (specializes_or_disjoint_nhds : ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)) : R1Space X
• R1Space.specializes_or_disjoint_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : R1Space X] (x y : X) : x ⤳ y ∨ Disjoint (nhds x) (nhds y)
• disjoint_nhds_nhds_iff_not_specializes 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : Disjoint (nhds x) (nhds y) ↔ ¬x ⤳ y
• r1Space_iff_specializes_or_disjoint_nhds 📋 Mathlib.Topology.Separation.Basic
  (X : Type u_3) [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)
• specializes_iff_not_disjoint 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {x y : X} : x ⤳ y ↔ ¬Disjoint (nhds x) (nhds y)
• t1Space_TFAE 📋 Mathlib.Topology.Separation.Basic
  (X : Type u) [TopologicalSpace X] : [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of, ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ nhds x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
• IsDiscrete.eq_of_specializes 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsDiscrete s) {a b : X} (hab : a ⤳ b) (ha : a ∈ s) (hb : b ∈ s) : a = b
• Disjoint.eventually_nhdsWithin_specializes 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {p : X} {s : Set X} (hs : Disjoint (nhdsWithin p s) Filter.cofinite) : ∀ᶠ (x : X) in nhdsWithin p s, x ⤳ p
• Disjoint.nhdsWithin_eq_of_cofinite 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} [TopologicalSpace X] {p : X} {s : Set X} (hs : Disjoint (nhdsWithin p s) Filter.cofinite) : nhdsWithin p s = Filter.principal ({x | x ⤳ p} ∩ s)
• Specializes.const_smul 📋 Mathlib.Topology.Algebra.ConstMulAction
  {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [SMul M α] [ContinuousConstSMul M α] {x y : α} (h : x ⤳ y) (c : M) : (c • x) ⤳ (c • y)
• Specializes.const_vadd 📋 Mathlib.Topology.Algebra.ConstMulAction
  {M : Type u_1} {α : Type u_2} [TopologicalSpace α] [VAdd M α] [ContinuousConstVAdd M α] {x y : α} (h : x ⤳ y) (c : M) : (c +ᵥ x) ⤳ (c +ᵥ y)
• Specializes.smul 📋 Mathlib.Topology.Algebra.MulAction
  {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [SMul M X] [ContinuousSMul M X] {a b : M} {x y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) : (a • x) ⤳ (b • y)
• Specializes.vadd 📋 Mathlib.Topology.Algebra.MulAction
  {M : Type u_1} {X : Type u_2} [TopologicalSpace M] [TopologicalSpace X] [VAdd M X] [ContinuousVAdd M X] {a b : M} {x y : X} (h₁ : a ⤳ b) (h₂ : x ⤳ y) : (a +ᵥ x) ⤳ (b +ᵥ y)
• ContinuousMap.map_specializes 📋 Mathlib.Topology.ContinuousMap.Basic
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y
• Specializes.add 📋 Mathlib.Topology.Algebra.Monoid
  {M : Type u_3} [TopologicalSpace M] [Add M] [ContinuousAdd M] {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) : (a + c) ⤳ (b + d)
• Specializes.mul 📋 Mathlib.Topology.Algebra.Monoid
  {M : Type u_3} [TopologicalSpace M] [Mul M] [ContinuousMul M] {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) : (a * c) ⤳ (b * d)
• Specializes.nsmul 📋 Mathlib.Topology.Algebra.Monoid
  {M : Type u_6} [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] {a b : M} (h : a ⤳ b) (n : ℕ) : (n • a) ⤳ (n • b)
• Specializes.pow 📋 Mathlib.Topology.Algebra.Monoid
  {M : Type u_6} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : a ⤳ b) (n : ℕ) : (a ^ n) ⤳ (b ^ n)
• Filter.HasBasis.specializes_iff_uniformity 📋 Mathlib.Topology.UniformSpace.Separation
  {α : Type u} [UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {x y : α} : x ⤳ y ↔ ∀ (i : ι), p i → (x, y) ∈ s i
• Specializes.inv 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {G : Type u_1} [TopologicalSpace G] [Inv G] [ContinuousInv G] {x y : G} (h : x ⤳ y) : x⁻¹ ⤳ y⁻¹
• Specializes.neg 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {G : Type u_1} [TopologicalSpace G] [Neg G] [ContinuousNeg G] {x y : G} (h : x ⤳ y) : (-x) ⤳ (-y)
• Specializes.zpow 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {G : Type u_4} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G} (h : x ⤳ y) (m : ℤ) : (x ^ m) ⤳ (y ^ m)
• Specializes.zsmul 📋 Mathlib.Topology.Algebra.Group.ContinuousInv
  {G : Type u_4} [SubNegMonoid G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousNeg G] {x y : G} (h : x ⤳ y) (m : ℤ) : (m • x) ⤳ (m • y)
• genericPoint_specializes 📋 Mathlib.Topology.Sober
  {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] (x : α) : genericPoint α ⤳ x
• IsGenericPoint.specializes 📋 Mathlib.Topology.Sober
  {α : Type u_1} [TopologicalSpace α] {x y : α} {S : Set α} (h : IsGenericPoint x S) (h' : y ∈ S) : x ⤳ y
• IsGenericPoint.specializes_iff_mem 📋 Mathlib.Topology.Sober
  {α : Type u_1} [TopologicalSpace α] {x y : α} {S : Set α} (h : IsGenericPoint x S) : x ⤳ y ↔ y ∈ S
• isGenericPoint_iff_specializes 📋 Mathlib.Topology.Sober
  {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} : IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
• IsLocalRing.specializes_closedPoint 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] [IsLocalRing R] (x : PrimeSpectrum R) : x ⤳ IsLocalRing.closedPoint R
• PrimeSpectrum.le_iff_specializes 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] (x y : PrimeSpectrum R) : x ≤ y ↔ x ⤳ y
• PrimeSpectrum.localizationMapOfSpecializes 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] {x y : PrimeSpectrum R} (h : x ⤳ y) : Localization.AtPrime y.asIdeal →+* Localization.AtPrime x.asIdeal
• TopCat.Presheaf.stalkSpecializes 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) : F.stalk y ⟶ F.stalk x
• TopCat.Presheaf.stalkSpecializes_comp 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (F.stalkSpecializes h) = F.stalkSpecializes ⋯
• TopCat.Presheaf.stalkSpecializes_comp_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h') (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (F.stalkSpecializes ⋯) h✝
• TopCat.Presheaf.germ_stalkSpecializes 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.germ U y hy) (F.stalkSpecializes h) = F.germ U x ⋯
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) ((TopCat.Presheaf.stalkFunctor C x).map f) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (G.stalkSpecializes h)
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {Z : C} (h✝ : (TopCat.Presheaf.stalkFunctor C x).obj G ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) (CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C x).map f) h✝) = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (CategoryTheory.CategoryStruct.comp (G.stalkSpecializes h) h✝)
• TopCat.Presheaf.germ_stalkSpecializes_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.germ U y hy) (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (F.germ U x ⋯) h✝
• TopCat.Presheaf.stalkSpecializes_comp_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {x y z : ↑X} (h : x ⤳ y) (h' : y ⤳ z) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x✝ : carrier (F.stalk z)) : (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h')) x✝) = (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes ⋯)) x✝
• TopCat.Presheaf.stalkSpecializes_stalkPushforward 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯) (TopCat.Presheaf.stalkPushforward C f F x) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y) (F.stalkSpecializes h)
• TopCat.Presheaf.stalkSpecializes_stalkFunctor_map_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x✝ : carrier (F.stalk y)) : (CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C x).map f)) ((CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) x✝) = (CategoryTheory.ConcreteCategory.hom (G.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor C y).map f)) x✝)
• TopCat.Presheaf.stalkSpecializes_stalkPushforward_assoc 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) {Z : C} (h✝ : F.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F x) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkPushforward C f F y) (CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) h✝)
• TopCat.Presheaf.germ_stalkSpecializes_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : TopCat} (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {y : ↑X} (hy : y ∈ U) {x : ↑X} (h : x ⤳ y) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x✝ : carrier (F.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (F.germ U y hy)) x✝) = (CategoryTheory.ConcreteCategory.hom (F.germ U x ⋯)) x✝
• TopCat.Presheaf.stalkSpecializes_stalkPushforward_apply 📋 Mathlib.Topology.Sheaves.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x✝ : carrier (((TopCat.Presheaf.pushforward C f).obj F).stalk ((TopCat.Hom.hom f) y))) : (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.stalkPushforward C f F x)) ((CategoryTheory.ConcreteCategory.hom (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯)) x✝) = (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.stalkPushforward C f F y)) x✝)
• ContinuousMap.specializes_coe 📋 Mathlib.Topology.CompactOpen
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g
• Specializes.joinedIn 📋 Mathlib.Topology.Connected.PathConnected
  {X : Type u_1} [TopologicalSpace X] {x y : X} {F : Set X} (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y
• mem_nhdsKer_singleton 📋 Mathlib.Topology.NhdsKer
  {X : Type u_2} [TopologicalSpace X] {x y : X} : x ∈ nhdsKer {y} ↔ x ⤳ y
• mem_nhdsKer_iff_specializes 📋 Mathlib.Topology.NhdsKer
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} : x ∈ nhdsKer s ↔ ∃ y ∈ s, x ⤳ y
• specializes_iff_nhdsKer_subset 📋 Mathlib.Topology.NhdsKer
  {X : Type u_2} [TopologicalSpace X] {x y : X} : x ⤳ y ↔ nhdsKer {x} ⊆ nhdsKer {y}
• isOpen_iff_forall_specializes 📋 Mathlib.Topology.AlexandrovDiscrete
  {α : Type u_3} [TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α} : IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s
• AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y) (X.presheaf.stalkSpecializes h)
• AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {Z : C} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)
• AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x✝ : carrier (Y.presheaf.stalk ((TopCat.Hom.hom f.base) y))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) x✝) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)) x✝)
• AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x') (X.presheaf.stalkSpecializes h)
• AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') {Z : CommRingCat} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x') (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)
• AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x')) y)
• AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes 📋 Mathlib.AlgebraicGeometry.StructureSheaf
  {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R y) ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h) = AlgebraicGeometry.StructureSheaf.toStalk R x
• AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_assoc 📋 Mathlib.AlgebraicGeometry.StructureSheaf
  {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) {Z : CommRingCat} (h✝ : (AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R y) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R x) h✝
• AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply 📋 Mathlib.AlgebraicGeometry.StructureSheaf
  {R : Type u_1} [CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) (x✝ : R) : (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R y)) x✝) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)) x✝
• AlgebraicGeometry.Scheme.le_iff_specializes 📋 Mathlib.AlgebraicGeometry.Scheme
  {X : AlgebraicGeometry.Scheme} {a b : ↥X} : a ≤ b ↔ b ⤳ a
• AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap 📋 Mathlib.AlgebraicGeometry.Scheme
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x') (X.presheaf.stalkSpecializes h)
• AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc 📋 Mathlib.AlgebraicGeometry.Scheme
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') {Z : CommRingCat} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap f x') (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)
• AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply 📋 Mathlib.AlgebraicGeometry.Scheme
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x')) y)
• AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf 📋 Mathlib.AlgebraicGeometry.Stalk
  {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y) : AlgebraicGeometry.Scheme.Hom.IsOver (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) X
• AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
  {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) = X.fromSpecStalk x
• AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk_assoc 📋 Mathlib.AlgebraicGeometry.Stalk
  {X : AlgebraicGeometry.Scheme} {x y : ↥X} (h : x ⤳ y) {Z : AlgebraicGeometry.Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h✝
• AlgebraicGeometry.Scheme.range_fromSpecStalk 📋 Mathlib.AlgebraicGeometry.Stalk
  {X : AlgebraicGeometry.Scheme} {x : ↥X} : Set.range ⇑(X.fromSpecStalk x) = {y | y ⤳ x}
• TopologicalSpace.vietoris.specializes_closure 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s : Set α} : s ⤳ closure s
• TopologicalSpace.vietoris.subset_closure_of_specializes 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} (h : s ⤳ t) : t ⊆ closure s
• TopologicalSpace.vietoris.subset_of_specializes 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} [T1Space α] (h : s ⤳ t) : s ⊆ t
• TopologicalSpace.vietoris.specializes_of_subset_closure 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hst : s ⊆ t) (hts : t ⊆ closure s) : s ⤳ t
• TopologicalSpace.vietoris.specializes_iff_of_t1Space 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} [T1Space α] : s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure s
• TopologicalSpace.vietoris.specializes_iff 📋 Mathlib.Topology.Sets.VietorisTopology
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} : s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure s
• OnePoint.not_specializes_infty_coe 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} [TopologicalSpace X] {x : X} : ¬OnePoint.infty ⤳ ↑x
• OnePoint.specializes_coe 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} [TopologicalSpace X] {x y : X} : ↑x ⤳ ↑y ↔ x ⤳ y
• Filter.specializes_iff_le 📋 Mathlib.Topology.Filter
  {α : Type u_2} {l₁ l₂ : Filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂
• Topology.IsLowerSet.specializes_iff_le 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLowerSet α] {a b : α} : a ⤳ b ↔ a ≤ b
• Topology.IsUpperSet.specializes_iff_le 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpperSet α] {a b : α} : a ⤳ b ↔ b ≤ a
• Topology.WithLowerSet.toLowerSet_specializes_toLowerSet 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] {a b : α} : Topology.WithLowerSet.toLowerSet a ⤳ Topology.WithLowerSet.toLowerSet b ↔ a ≤ b
• Topology.WithUpperSet.toUpperSet_specializes_toUpperSet 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] {a b : α} : Topology.WithUpperSet.toUpperSet a ⤳ Topology.WithUpperSet.toUpperSet b ↔ b ≤ a
• Topology.WithLowerSet.ofLowerSet_le_ofLowerSet 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] {a b : Topology.WithLowerSet α} : Topology.WithLowerSet.ofLowerSet a ≤ Topology.WithLowerSet.ofLowerSet b ↔ a ⤳ b
• Topology.WithUpperSet.ofUpperSet_le_ofUpperSet 📋 Mathlib.Topology.Order.UpperLowerSetTopology
  {α : Type u_1} [Preorder α] {a b : Topology.WithUpperSet α} : Topology.WithUpperSet.ofUpperSet a ≤ Topology.WithUpperSet.ofUpperSet b ↔ b ⤳ a
• Specialization.toEquiv_le_toEquiv 📋 Mathlib.Topology.Specialization
  {α : Type u_1} [TopologicalSpace α] {a b : α} : Specialization.toEquiv a ≤ Specialization.toEquiv b ↔ b ⤳ a
• Specialization.ofEquiv_specializes_ofEquiv 📋 Mathlib.Topology.Specialization
  {α : Type u_1} [TopologicalSpace α] {a b : Specialization α} : Specialization.ofEquiv a ⤳ Specialization.ofEquiv b ↔ b ≤ a
• skyscraperPresheafStalkOfNotSpecializesIsTerminal 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : ¬p₀ ⤳ y) : CategoryTheory.Limits.IsTerminal ((skyscraperPresheaf p₀ A).stalk y)
• skyscraperPresheafStalkOfSpecializes 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) : (skyscraperPresheaf p₀ A).stalk y ≅ A
• skyscraperPresheafStalkOfNotSpecializes 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : ¬p₀ ⤳ y) : (skyscraperPresheaf p₀ A).stalk y ≅ ⊤_ C
• skyscraperPresheafCoconeOfSpecializes 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A))
• skyscraperPresheafCoconeIsColimitOfNotSpecializes 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : ¬p₀ ⤳ y) : CategoryTheory.Limits.IsColimit (skyscraperPresheafCocone p₀ A y)
• skyscraperPresheafCoconeIsColimitOfSpecializes 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : CategoryTheory.Limits.IsColimit (skyscraperPresheafCoconeOfSpecializes p₀ A h)
• skyscraperPresheafCoconeOfSpecializes_pt 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : (skyscraperPresheafCoconeOfSpecializes p₀ A h).pt = A
• germ_skyscraperPresheafStalkOfSpecializes_hom 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U) : CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU) (skyscraperPresheafStalkOfSpecializes p₀ A h).hom = CategoryTheory.eqToHom ⋯
• germ_skyscraperPresheafStalkOfSpecializes_hom_assoc 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU) (CategoryTheory.CategoryStruct.comp (skyscraperPresheafStalkOfSpecializes p₀ A h).hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝
• skyscraperPresheafCoconeOfSpecializes_ι_app 📋 Mathlib.Topology.Sheaves.Skyscraper
  {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) (U : (TopologicalSpace.OpenNhds y)ᵒᵖ) : (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U = CategoryTheory.eqToHom ⋯
• Opens.pointGrothendieckTopologyHomEquiv 📋 Mathlib.Topology.Sheaves.Points
  {X : Type u} [TopologicalSpace X] {x y : X} : (Opens.pointGrothendieckTopology x ⟶ Opens.pointGrothendieckTopology y) ≃ x ⤳ y

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