Loogle!

Result

Found 258 declarations mentioning Topology.IsOpenEmbedding. Of these, only the first 200 are shown.

• Topology.IsOpenEmbedding 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Prop
• Topology.IsOpenEmbedding.toIsEmbedding 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : Topology.IsOpenEmbedding f) : Topology.IsEmbedding f
• Topology.IsOpenEmbedding.isOpen_range 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : Topology.IsOpenEmbedding f) : IsOpen (Set.range f)
• Topology.IsOpenEmbedding.mk 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (toIsEmbedding : Topology.IsEmbedding f) (isOpen_range : IsOpen (Set.range f)) : Topology.IsOpenEmbedding f
• Topology.isOpenEmbedding_iff 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Topology.IsOpenEmbedding f ↔ Topology.IsEmbedding f ∧ IsOpen (Set.range f)
• Topology.IsOpenEmbedding.id 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} [TopologicalSpace X] : Topology.IsOpenEmbedding id
• Topology.IsOpenEmbedding.of_isEmpty 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] (f : X → Y) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.continuous 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) : Continuous f
• Topology.IsOpenEmbedding.isEmbedding 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) : Topology.IsEmbedding f
• Topology.IsOpenEmbedding.isInducing 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) : Topology.IsInducing f
• Topology.IsOpenEmbedding.isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) : IsOpenMap f
• Topology.IsEmbedding.isOpenEmbedding_of_surjective 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (hsurj : Function.Surjective f) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.of_isEmbedding 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (hsurj : Function.Surjective f) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.of_isEmbedding_isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Topology.IsEmbedding f) (h₂ : IsOpenMap f) : Topology.IsOpenEmbedding f
• Topology.isOpenEmbedding_iff_isEmbedding_isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding f ↔ Topology.IsEmbedding f ∧ IsOpenMap f
• Topology.IsOpenEmbedding.isOpen_iff_image_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s)
• Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (h₁ : Continuous f) (h₂ : Function.Injective f) (h₃ : IsOpenMap f) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) (x : X) : Filter.map f (nhds x) = nhds (f x)
• Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f
• Topology.IsOpenEmbedding.accPt_comap_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {x : X} {l : Filter Y} : AccPt x (Filter.comap f l) ↔ AccPt (f x) l
• Topology.IsOpenEmbedding.comp 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Topology.IsOpenEmbedding g) (hf : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (g ∘ f)
• Topology.IsOpenEmbedding.of_comp 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (hg : Topology.IsOpenEmbedding g) (h : Topology.IsOpenEmbedding (g ∘ f)) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.isOpenMap_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hg : Topology.IsOpenEmbedding g) : IsOpenMap f ↔ IsOpenMap (g ∘ f)
• Topology.IsOpenEmbedding.of_comp_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Y) (hg : Topology.IsOpenEmbedding g) : Topology.IsOpenEmbedding (g ∘ f) ↔ Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) : IsOpen s ↔ IsOpen (f ⁻¹' s)
• Topology.IsOpenEmbedding.continuousAt_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (hf : Topology.IsOpenEmbedding f) {x : X} : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
• Topology.IsOpenEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
  {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsOpenEmbedding g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))
• Topology.IsOpenEmbedding.tendsto_nhds_iff' 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {l : Filter Z} {x : X} : Filter.Tendsto (g ∘ f) (nhds x) l ↔ Filter.Tendsto g (nhds (f x)) l
• Topology.IsOpenEmbedding.image_mem_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) {s : Set X} {x : X} : f '' s ∈ nhds (f x) ↔ s ∈ nhds x
• Homeomorph.isOpenEmbedding 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : Topology.IsOpenEmbedding ⇑h
• Homeomorph.comp_isOpenEmbedding_iff 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : Y ≃ₜ Z) {f : X → Y} : Topology.IsOpenEmbedding (⇑e ∘ f) ↔ Topology.IsOpenEmbedding f
• Homeomorph.isOpenEmbedding_comp_iff 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) {f : Y → Z} : Topology.IsOpenEmbedding (f ∘ ⇑e) ↔ Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.inl 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inl
• Topology.IsOpenEmbedding.inr 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.inr
• Topology.IsOpenEmbedding.sumSwap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsOpenEmbedding Sum.swap
• Topology.IsOpenEmbedding.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) : Topology.IsOpenEmbedding (Prod.map f g)
• Topology.IsOpenEmbedding.sumElim 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Z} {g : Y → Z} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) (h : Function.Injective (Sum.elim f g)) : Topology.IsOpenEmbedding (Sum.elim f g)
• Topology.IsOpenEmbedding.sigmaMk 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : Topology.IsOpenEmbedding (Sigma.mk i)
• IsOpen.isOpenEmbedding_subtypeVal 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : Topology.IsOpenEmbedding Subtype.val
• Topology.IsOpenEmbedding.piMap 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {A : ι → Type u_3} {B : ι → Type u_4} [T : (i : ι) → TopologicalSpace (A i)] [(i : ι) → TopologicalSpace (B i)] [Finite ι] {f : (i : ι) → A i → B i} (hf : ∀ (i : ι), Topology.IsOpenEmbedding (f i)) : Topology.IsOpenEmbedding (Pi.map f)
• Topology.isOpenEmbedding_sigmaMap 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {κ : Type u_3} {σ : ι → Type u_4} {τ : κ → Type u_5} [(i : ι) → TopologicalSpace (σ i)] [(k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)} (h : Function.Injective f₁) : Topology.IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Topology.IsOpenEmbedding (f₂ i)
• Topology.IsOpenEmbedding.restrict 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) {s : Set X} {t : Set Y} (H : Set.MapsTo f s t) (hs : IsOpen s) : Topology.IsOpenEmbedding (Set.MapsTo.restrict f s t H)
• Topology.IsOpenEmbedding.inclusion 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) (hs : IsOpen (Subtype.val ⁻¹' s)) : Topology.IsOpenEmbedding (Set.inclusion hst)
• Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsOpenEmbedding f) (s : Set β) (x : α) : Filter.map f (nhdsWithin x (f ⁻¹' s)) = nhdsWithin (f x) s
• Topology.IsOpenEmbedding.separableSpace 📋 Mathlib.Topology.Bases
  {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace.SeparableSpace β] {f : α → β} (h : Topology.IsOpenEmbedding f) : TopologicalSpace.SeparableSpace α
• Topology.IsOpenEmbedding.locallyCompactSpace 📋 Mathlib.Topology.Compactness.LocallyCompact
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) : LocallyCompactSpace X
• Topology.IsOpenEmbedding.generalizingMap 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) : GeneralizingMap f
• Topology.IsOpenEmbedding.preirreducibleSpace 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsOpenEmbedding f) [PreirreducibleSpace X] : PreirreducibleSpace Y
• Topology.IsOpenEmbedding.irreducibleSpace 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Topology.IsOpenEmbedding f) [IrreducibleSpace X] [Nonempty Y] : IrreducibleSpace Y
• IsPreirreducible.preimage 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set X} (ht : IsPreirreducible t) {f : Y → X} (hf : Topology.IsOpenEmbedding f) : IsPreirreducible (f ⁻¹' t)
• IsIrreducible.preimage 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set X} (ht : IsIrreducible t) {f : Y → X} (hf : Topology.IsOpenEmbedding f) (h : (t ∩ Set.range f).Nonempty) : IsIrreducible (f ⁻¹' t)
• preimage_mem_irreducibleComponents 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {t : Set X} (ht : t ∈ irreducibleComponents X) {f : Y → X} (hf : Topology.IsOpenEmbedding f) (h : (t ∩ Set.range f).Nonempty) : f ⁻¹' t ∈ irreducibleComponents Y
• separated_by_isOpenEmbedding 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : X → Y} (hf : Topology.IsOpenEmbedding f) {x y : X} (h : x ≠ y) : ∃ u v, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v
• Topology.IsOpenEmbedding.locallyConnectedSpace 📋 Mathlib.Topology.Connected.LocallyConnected
  {α : Type u} {β : Type v} [TopologicalSpace α] [LocallyConnectedSpace α] [TopologicalSpace β] {f : β → α} (h : Topology.IsOpenEmbedding f) : LocallyConnectedSpace β
• Topology.IsOpenEmbedding.baireSpace 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {Y : Type u_4} [TopologicalSpace Y] {p : Y → X} (hp : Topology.IsOpenEmbedding p) : BaireSpace Y
• IsHomeomorph.isOpenEmbedding 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsHomeomorph f) : Topology.IsOpenEmbedding f
• Topology.IsOpenEmbedding.uliftMap 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (ULift.map f)
• TopologicalSpace.Opens.isOpenEmbedding' 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) : Topology.IsOpenEmbedding Subtype.val
• TopologicalSpace.Opens.isOpenEmbedding_of_le 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] {U V : TopologicalSpace.Opens α} (i : U ≤ V) : Topology.IsOpenEmbedding (Set.inclusion ⋯)
• Topology.IsOpenEmbedding.coborder_preimage 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) (s : Set Y) : coborder (f ⁻¹' s) = f ⁻¹' coborder s
• Set.restrictPreimage_isOpenEmbedding 📋 Mathlib.Topology.LocalAtTarget
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (s.restrictPreimage f)
• Topology.IsOpenEmbedding.restrictPreimage 📋 Mathlib.Topology.LocalAtTarget
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (s : Set β) (h : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding (s.restrictPreimage f)
• TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage 📋 Mathlib.Topology.LocalAtTarget
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : TopologicalSpace.IsOpenCover U) (h : Continuous f) : Topology.IsOpenEmbedding f ↔ ∀ (i : ι), Topology.IsOpenEmbedding ((U i).carrier.restrictPreimage f)
• TopologicalSpace.IrreducibleCloseds.orderIsoOfIsOpenEmbedding 📋 Mathlib.Topology.Sets.Closeds
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : β → α) (h : Topology.IsOpenEmbedding f) : TopologicalSpace.IrreducibleCloseds β ≃o ↑{V | (f ⁻¹' ↑V).Nonempty}
• QuasiSeparatedSpace.of_isOpenEmbedding 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] {f : β → α} (h : Topology.IsOpenEmbedding f) : QuasiSeparatedSpace β
• Topology.IsOpenEmbedding.quasiSeparatedSpace 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} [QuasiSeparatedSpace β] (h : Topology.IsOpenEmbedding f) : QuasiSeparatedSpace α
• Topology.IsOpenEmbedding.isQuasiSeparated_iff 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : Topology.IsOpenEmbedding f) {s : Set α} : IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s)
• Topology.IsOpenEmbedding.prespectralSpace 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PrespectralSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) : PrespectralSpace X
• IsRetrocompact.preimage_of_isOpenEmbedding 📋 Mathlib.Topology.Constructible
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hf : Topology.IsOpenEmbedding f) (hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s)
• Topology.IsConstructible.preimage_of_isOpenEmbedding 📋 Mathlib.Topology.Constructible
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hf : Topology.IsOpenEmbedding f) (hs : Topology.IsConstructible s) : Topology.IsConstructible (f ⁻¹' s)
• Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding 📋 Mathlib.Topology.Constructible
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : Topology.IsLocallyConstructible s) (hf : Topology.IsOpenEmbedding f) : Topology.IsLocallyConstructible (f ⁻¹' s)
• Topology.IsConstructible.image_of_isOpenEmbedding 📋 Mathlib.Topology.Constructible
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hfopen : Topology.IsOpenEmbedding f) (hfcomp : IsRetrocompact (Set.range f)) (hs : Topology.IsConstructible s) : Topology.IsConstructible (f '' s)
• Topology.isConstructible_preimage_iff_of_isOpenEmbedding 📋 Mathlib.Topology.Constructible
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hf : Topology.IsOpenEmbedding f) (hfcomp : IsRetrocompact (Set.range f)) (hsf : s ⊆ Set.range f) : Topology.IsConstructible (f ⁻¹' s) ↔ Topology.IsConstructible s
• Topology.IsOpenEmbedding.quasiSober 📋 Mathlib.Topology.Sober
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsOpenEmbedding f) [QuasiSober β] : QuasiSober α
• Topology.IsOpenEmbedding.coheight_eq 📋 Mathlib.Topology.KrullDimension
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [QuasiSober Y] [T0Space Y] [QuasiSober X] [T0Space X] {x : X} (f : X → Y) (hf : Topology.IsOpenEmbedding f) : Order.coheight (f x) = Order.coheight x
• Topology.IsOpenEmbedding.coheight_map 📋 Mathlib.Topology.KrullDimension
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) (Z : TopologicalSpace.IrreducibleCloseds X) : Order.coheight (TopologicalSpace.IrreducibleCloseds.map f ⋯ Z) = Order.coheight Z
• Topology.IsOpenEmbedding.spectralSpace 📋 Mathlib.Topology.Spectral.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [SpectralSpace Y] [CompactSpace X] (hf : Topology.IsOpenEmbedding f) : SpectralSpace X
• PrimeSpectrum.localization_away_isOpenEmbedding 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] (S : Type v) [CommSemiring S] [Algebra R S] (r : R) [IsLocalization.Away r S] : Topology.IsOpenEmbedding (PrimeSpectrum.comap (algebraMap R S))
• PrimeSpectrum.isOpenEmbedding_sigmaToPi 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {ι : Type u_1} (R : ι → Type u_2) [(i : ι) → CommRing (R i)] : Topology.IsOpenEmbedding (PrimeSpectrum.sigmaToPi R)
• TopCat.isOpenEmbedding_iff_comp_isIso 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)
• TopCat.isOpenEmbedding_iff_isIso_comp 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)
• TopCat.isOpenEmbedding_iff_comp_isIso' 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso g] : Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)
• TopCat.isOpenEmbedding_iff_isIso_comp' 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : Topology.IsOpenEmbedding (⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)
• TopCat.binaryCofan_isColimit_iff 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {X Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧ IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))
• TopCat.fst_isOpenEmbedding_of_right 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
  {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
• TopCat.snd_isOpenEmbedding_of_left 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
  {X Y S : TopCat} {f : X ⟶ S} (H : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (g : Y ⟶ S) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
• TopCat.isOpenEmbedding_of_pullback 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
  {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (H₂ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))
• TopCat.pullback_map_isOpenEmbedding 📋 Mathlib.Topology.Category.TopCat.Limits.Pullbacks
  {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁)) (H₂ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₂)) (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃] (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))
• Topology.IsOpenEmbedding.functor 📋 Mathlib.Topology.Category.TopCat.Opens
  {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)
• TopologicalSpace.Opens.instPreservesLimitsOfShapeCarrierDiscreteFunctorOfNonemptyOfFinite 📋 Mathlib.Topology.Category.TopCat.Opens
  {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {ι : Type u_1} [Nonempty ι] [Finite ι] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete ι) hf.functor
• Topology.IsOpenEmbedding.functor_obj_injective 📋 Mathlib.Topology.Category.TopCat.Opens
  {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : Function.Injective hf.functor.obj
• TopologicalSpace.Opens.map_functor_eq' 📋 Mathlib.Topology.Category.TopCat.Opens
  {X U : TopCat} (f : U ⟶ X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) : (TopologicalSpace.Opens.map f).obj (hf.functor.obj V) = V
• TopologicalSpace.Opens.isOpenEmbedding 📋 Mathlib.Topology.Category.TopCat.Opens
  {X : TopCat} (U : TopologicalSpace.Opens ↑X) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom U.inclusion')
• Topology.IsOpenEmbedding.functor_obj_iInf 📋 Mathlib.Topology.Category.TopCat.Opens
  {X Y : TopCat} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {ι : Type u_1} [Nonempty ι] [Finite ι] (g : ι → TopologicalSpace.Opens ↑X) : hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i)
• Topology.IsOpenEmbedding.functorNhds 📋 Mathlib.Topology.Category.TopCat.OpenNhds
  {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.OpenNhds ((CategoryTheory.ConcreteCategory.hom f) x))
• Topology.IsOpenEmbedding.adjunctionNhds 📋 Mathlib.Topology.Category.TopCat.OpenNhds
  {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X) : ⋯.functorNhds x ⊣ TopologicalSpace.OpenNhds.map f x
• TopologicalSpace.OpenNhds.isOpenEmbedding 📋 Mathlib.Topology.Category.TopCat.OpenNhds
  {X : TopCat} {x : ↑X} (U : TopologicalSpace.OpenNhds x) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (↑U).inclusion')
• Topology.IsOpenEmbedding.compatiblePreserving 📋 Mathlib.Topology.Sheaves.SheafCondition.Sites
  {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.CompatiblePreserving (Opens.grothendieckTopology ↑Y) hf.functor
• Topology.IsOpenEmbedding.functor_isContinuous 📋 Mathlib.Topology.Sheaves.SheafCondition.Sites
  {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : h.functor.IsContinuous (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y)
• TopCat.Presheaf.isSheaf_of_isOpenEmbedding 📋 Mathlib.Topology.Sheaves.SheafCondition.Sites
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : TopCat} {f : X ⟶ Y} {F : TopCat.Presheaf C Y} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (hF : F.IsSheaf) : TopCat.Presheaf.IsSheaf (h.functor.op.comp F)
• JacobsonSpace.of_isOpenEmbedding 📋 Mathlib.Topology.JacobsonSpace
  {X : Type u_2} {Y : Type u_1} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [JacobsonSpace Y] (hf : Topology.IsOpenEmbedding f) : JacobsonSpace X
• Topology.IsOpenEmbedding.preimage_closedPoints 📋 Mathlib.Topology.JacobsonSpace
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) [JacobsonSpace Y] : f ⁻¹' closedPoints Y = closedPoints X
• ENNReal.isOpenEmbedding_coe 📋 Mathlib.Topology.Algebra.Ring.Real
  : Topology.IsOpenEmbedding ENNReal.ofNNReal
• EReal.isOpenEmbedding_coe 📋 Mathlib.Topology.Instances.EReal.Lemmas
  : Topology.IsOpenEmbedding Real.toEReal
• Topology.IsOpenEmbedding.measurableEmbedding 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α] [mβ : TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {f : α → β} (h : Topology.IsOpenEmbedding f) : MeasurableEmbedding f
• MeasureTheory.Measure.IsOpenPosMeasure.comap 📋 Mathlib.MeasureTheory.Measure.OpenPos
  {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} [BorelSpace X] {Z : Type u_3} [TopologicalSpace Z] {mZ : MeasurableSpace Z} [BorelSpace Z] (μ : MeasureTheory.Measure Z) [μ.IsOpenPosMeasure] {f : X → Z} (hf : Topology.IsOpenEmbedding f) : (MeasureTheory.Measure.comap f μ).IsOpenPosMeasure
• MeasureTheory.Measure.InnerRegular.comap' 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] {mβ : MeasurableSpace β} [TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [H : μ.InnerRegular] {f : α → β} (hf : Topology.IsOpenEmbedding f) : (MeasureTheory.Measure.comap f μ).InnerRegular
• MeasureTheory.Measure.Regular.comap' 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [TopologicalSpace α] [BorelSpace α] {mβ : MeasurableSpace β} [TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [μ.Regular] {f : α → β} (hf : Topology.IsOpenEmbedding f) : (MeasureTheory.Measure.comap f μ).Regular
• MeasureTheory.Measure.IsAddHaarMeasure.comap 📋 Mathlib.MeasureTheory.Group.Measure
  {G : Type u_1} {H : Type u_2} [MeasurableSpace G] [MeasurableSpace H] [AddGroup G] [TopologicalSpace G] [BorelSpace G] [MeasurableAdd G] [AddGroup H] [TopologicalSpace H] [BorelSpace H] {mH : MeasurableAdd H} (μ : MeasureTheory.Measure H) [μ.IsAddHaarMeasure] {f : G →+ H} (hf : Topology.IsOpenEmbedding ⇑f) : (MeasureTheory.Measure.comap (⇑f) μ).IsAddHaarMeasure
• MeasureTheory.Measure.IsHaarMeasure.comap 📋 Mathlib.MeasureTheory.Group.Measure
  {G : Type u_1} {H : Type u_2} [MeasurableSpace G] [MeasurableSpace H] [Group G] [TopologicalSpace G] [BorelSpace G] [MeasurableMul G] [Group H] [TopologicalSpace H] [BorelSpace H] {mH : MeasurableMul H} (μ : MeasureTheory.Measure H) [μ.IsHaarMeasure] {f : G →* H} (hf : Topology.IsOpenEmbedding ⇑f) : (MeasureTheory.Measure.comap (⇑f) μ).IsHaarMeasure
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] : OpenPartialHomeomorph X Y
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_apply 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] : ↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h) = f
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] {x : X} : ↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm (f x) = x
• OpenPartialHomeomorph.isOpenEmbedding 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsOpenEmbedding ↑e
• OpenPartialHomeomorph.to_isOpenEmbedding 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsOpenEmbedding ↑e
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] : (Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).source = Set.univ
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] : (Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).target = Set.range f
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : Topology.IsOpenEmbedding f) [Nonempty X] {x : Y} (hx : x ∈ Set.range f) : f (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm x) = x
• OpenPartialHomeomorph.isOpenEmbedding_restrict 📋 Mathlib.Topology.OpenPartialHomeomorph.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Topology.IsOpenEmbedding (e.source.domRestrict ↑e)
• Real.isOpenEmbedding_exp 📋 Mathlib.Analysis.SpecialFunctions.Exp
  : Topology.IsOpenEmbedding Real.exp
• AffineMap.isOpenEmbedding_linear_iff 📋 Mathlib.Topology.Algebra.Affine
  {R : Type u_1} {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [AddCommGroup V] [TopologicalSpace V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [AddCommGroup W] [TopologicalSpace W] [AddTorsor W Q] [TopologicalSpace Q] [IsTopologicalAddTorsor Q] [Ring R] [Module R V] [Module R W] {f : P →ᵃ[R] Q} : Topology.IsOpenEmbedding ⇑f.linear ↔ Topology.IsOpenEmbedding ⇑f
• Topology.IsOpenEmbedding.locPathConnectedSpace 📋 Mathlib.Topology.Connected.LocallyPathConnected
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyPathConnectedSpace X] {e : Y → X} (he : Topology.IsOpenEmbedding e) : LocallyPathConnectedSpace Y
• Topology.IsOpenEmbedding.locallyPathConnectedSpace 📋 Mathlib.Topology.Connected.LocallyPathConnected
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyPathConnectedSpace X] {e : Y → X} (he : Topology.IsOpenEmbedding e) : LocallyPathConnectedSpace Y
• Units.isOpenEmbedding_val 📋 Mathlib.Analysis.Normed.Ring.Units
  {R : Type u_1} [NormedRing R] [HasSummableGeomSeries R] : Topology.IsOpenEmbedding Units.val
• Topology.IsOpenEmbedding.matrix_map 📋 Mathlib.Topology.Instances.Matrix
  {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [TopologicalSpace R] [TopologicalSpace S] {f : R → S} [Finite m] [Finite n] (hf : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding fun x => x.map f
• AlgebraicGeometry.PresheafedSpace.restrict 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.PresheafedSpace C
• AlgebraicGeometry.PresheafedSpace.restrict_carrier 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h) = U
• AlgebraicGeometry.PresheafedSpace.ofRestrict_mono 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) (f : U ⟶ ↑X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Mono (X.ofRestrict hf)
• AlgebraicGeometry.PresheafedSpace.ofRestrict 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X
• AlgebraicGeometry.PresheafedSpace.ofRestrict_base 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.ofRestrict h).base = f
• AlgebraicGeometry.PresheafedSpace.restrict_presheaf 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.restrict h).presheaf = h.functor.op.comp X.presheaf
• AlgebraicGeometry.PresheafedSpace.ofRestrict_c_app 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ) : (X.ofRestrict h).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrict h).presheaf.stalk x ≅ X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x)
• AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x)
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrictStalkIso h x).inv = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ V x hx
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom = X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : C} (h✝ : (X.restrict h).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h✝) = CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h✝
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : C} (h✝ : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).hom h✝) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) h✝
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {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 (X.presheaf.obj (Opposite.op (h.functor.obj V)))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) x✝) = (CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) x✝
• AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply 📋 Mathlib.Geometry.RingedSpace.Stalks
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {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 ((X.restrict h).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom) ((CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) x✝) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) x✝
• Topology.IsOpenEmbedding.sheafPullback 📋 Mathlib.Topology.Sheaves.Functors
  {X Y : TopCat} (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.Functor (TopCat.Sheaf A Y) (TopCat.Sheaf A X)
• Topology.IsOpenEmbedding.sheafPullbackIso 📋 Mathlib.Topology.Sheaves.Functors
  {X Y : TopCat} (A : Type u_1) [CategoryTheory.Category.{w, u_1} A] {f : X ⟶ Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {FA : A → A → Type u_2} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [CategoryTheory.ConcreteCategory A FA] [CategoryTheory.Limits.HasColimits A] [CategoryTheory.Limits.HasLimits A] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)] [(CategoryTheory.forget A).ReflectsIsomorphisms] : TopCat.Sheaf.pullback A f ≅ Topology.IsOpenEmbedding.sheafPullback A hf
• AlgebraicGeometry.SheafedSpace.restrict 📋 Mathlib.Geometry.RingedSpace.SheafedSpace
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.SheafedSpace C
• AlgebraicGeometry.SheafedSpace.ofRestrict 📋 Mathlib.Geometry.RingedSpace.SheafedSpace
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X
• AlgebraicGeometry.SheafedSpace.ofRestrict_hom_base 📋 Mathlib.Geometry.RingedSpace.SheafedSpace
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.ofRestrict h).hom.base = f
• AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app 📋 Mathlib.Geometry.RingedSpace.SheafedSpace
  {C : Type u} [CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C) {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ) : (X.ofRestrict h).hom.c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
• AlgebraicGeometry.LocallyRingedSpace.restrict 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.LocallyRingedSpace
• AlgebraicGeometry.LocallyRingedSpace.ofRestrict 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X
• AlgebraicGeometry.LocallyRingedSpace.restrict_carrier 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h).toPresheafedSpace = U
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrict h).presheaf.stalk x ≅ X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x)
• AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x)
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrictStalkIso h x).inv = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x
• AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (X.restrict h).presheaf.obj X✝ = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X✝)))
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ V x hx
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom = X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : CommRingCat} (h✝ : (X.restrict h).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h✝) = CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h✝
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : CommRingCat} (h✝ : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).hom h✝) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) h✝
• AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ} (f✝ : X✝ ⟶ Y✝) : (X.restrict h).presheaf.map f✝ = X.presheaf.map (h.functor.map f✝.unop).op
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) (y : ↑((X.restrict h).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom) ((CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) y
• AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply 📋 Mathlib.Geometry.RingedSpace.LocallyRingedSpace
  {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) (y : ↑(X.presheaf.obj (Opposite.op (h.functor.obj V)))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) y) = (CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y
• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instOfRestrict 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (X.ofRestrict hf)
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : AlgebraicGeometry.PresheafedSpace C) {f : X ⟶ ↑Y} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (Y.ofRestrict hf)
• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {X : TopCat} (Y : AlgebraicGeometry.LocallyRingedSpace) {f : X ⟶ ↑Y.toPresheafedSpace} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (Y.ofRestrict hf)
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} (Y : AlgebraicGeometry.SheafedSpace C) {f : X ⟶ ↑Y.toPresheafedSpace} (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.SheafedSpace.IsOpenImmersion (Y.ofRestrict hf)
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.base_open 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} [self : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)
• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.of_stalk_iso 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)) [stalk_iso : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)] : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sigma_ι_isOpenEmbedding 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] {ι : Type v} (F : CategoryTheory.Functor (CategoryTheory.Discrete ι) (AlgebraicGeometry.SheafedSpace C)) [CategoryTheory.Limits.HasColimit F] (i : CategoryTheory.Discrete ι) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F i).hom.base)
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.HasColimits C] {FC : C → C → Type u_1} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC] [(CategoryTheory.forget C).ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)) [H : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)] : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h)) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mk 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} {f : X ⟶ Y} (base_open : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (c_iso : ∀ (U : TopologicalSpace.Opens ↑↑X), CategoryTheory.IsIso (f.c.app (Opposite.op (base_open.functor.obj U)))) : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f
• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) : AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U = CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
• AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h)) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U)))) x
• AlgebraicGeometry.SheafedSpace.IsOpenImmersion.ofRestrict_invApp_apply 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.SheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) {F : C → C → Type uF} {carrier : C → Type w_1} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x : carrier ((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U)))) x
• AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply 📋 Mathlib.Geometry.RingedSpace.OpenImmersion
  (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) (x : ↑((X.restrict h).presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U)) x = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U)))) x
• AlgebraicGeometry.Scheme.restrict 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.Scheme
• AlgebraicGeometry.IsOpenImmersion.ofRestrict 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : AlgebraicGeometry.IsOpenImmersion (X.ofRestrict h)
• AlgebraicGeometry.Scheme.ofRestrict 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X
• AlgebraicGeometry.Scheme.restrict_carrier 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h).toPresheafedSpace = U
• AlgebraicGeometry.Scheme.Hom.isOpenEmbedding 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : Topology.IsOpenEmbedding ⇑f
• AlgebraicGeometry.Scheme.restrict_toPresheafedSpace 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (X.restrict h).toPresheafedSpace = X.restrict h
• AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_base 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).base = f
• AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding ⇑f) [∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)] : AlgebraicGeometry.IsOpenImmersion f
• AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} : AlgebraicGeometry.IsOpenImmersion f ↔ Topology.IsOpenEmbedding ⇑f ∧ ∀ (x : ↥X), CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap f x)
• AlgebraicGeometry.Scheme.restrict_presheaf_obj 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (X.restrict h).presheaf.obj X✝ = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X✝)))
• AlgebraicGeometry.Scheme.ofRestrict_appIso 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U✝ : (X.restrict h).Opens) : AlgebraicGeometry.Scheme.Hom.appIso (X.ofRestrict h) U✝ = CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (X.ofRestrict h)).obj U✝)))
• AlgebraicGeometry.Scheme.ofRestrict_appLE 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) (W : (X.restrict h).Opens) (e : W ≤ (TopologicalSpace.Opens.map (X.ofRestrict h).base).obj V) : AlgebraicGeometry.Scheme.Hom.appLE (X.ofRestrict h) V W e = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
• AlgebraicGeometry.Scheme.restrict_presheaf_map 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V W : (TopologicalSpace.Opens ↥(X.restrict h))ᵒᵖ) (i : V ⟶ W) : (X.restrict h).presheaf.map i = X.presheaf.map (CategoryTheory.homOfLE ⋯).op
• AlgebraicGeometry.Scheme.ofRestrict_toLRSHom_c_app 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : (TopologicalSpace.Opens ↥X)ᵒᵖ) : (AlgebraicGeometry.Scheme.Hom.toLRSHom (X.ofRestrict h)).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
• AlgebraicGeometry.Scheme.ofRestrict_app 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : X.Opens) : AlgebraicGeometry.Scheme.Hom.app (X.ofRestrict h) V = X.presheaf.map (⋯.adjunction.counit.app V).op
• TopCat.GlueData.mk 📋 Mathlib.Topology.Gluing
  (toGlueData : CategoryTheory.GlueData TopCat) (f_open : ∀ (i j : toGlueData.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData.f i j))) : TopCat.GlueData
• TopCat.GlueData.f_open 📋 Mathlib.Topology.Gluing
  (self : TopCat.GlueData) (i j : self.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (self.f i j))
• TopCat.GlueData.ι_isOpenEmbedding 📋 Mathlib.Topology.Gluing
  (D : TopCat.GlueData) (i : D.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i))
• TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding 📋 Mathlib.Topology.Gluing
  {α : Type u} [TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U))
• AlgebraicGeometry.PresheafedSpace.GlueData.ι_isOpenEmbedding 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
  {C : Type u} [CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C) [CategoryTheory.Limits.HasLimits C] (i : D.J) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i).base)
• AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued 📋 Mathlib.AlgebraicGeometry.Gluing
  {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) : Topology.IsOpenEmbedding ⇑(AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰)
• AlgebraicGeometry.isOpenEmbedding_isZariskiLocalAtTarget 📋 Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  : AlgebraicGeometry.IsZariskiLocalAtTarget (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding)
• AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenEmbedding 📋 Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  : (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding).RespectsIso
• AlgebraicGeometry.isOpenImmersion_eq_inf 📋 Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
  : AlgebraicGeometry.IsOpenImmersion = (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Topology.IsOpenEmbedding) ⊓ AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] x => Function.Bijective ⇑x

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