Loogle!

Result

Found 112 definitions whose name contains "of_isOpen".

• Dense.inter_of_isOpen_left 📋 Mathlib.Topology.Basic
  {X : Type u} {s t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)
• Dense.inter_of_isOpen_right 📋 Mathlib.Topology.Basic
  {X : Type u} {s t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)
• DenseRange.subset_closure_image_preimage_of_isOpen 📋 Mathlib.Topology.Basic
  {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X} (hf : DenseRange f) (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s))
• TopologicalSpace.generateFrom_setOf_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} (t : TopologicalSpace α) : TopologicalSpace.generateFrom {s | IsOpen s} = t
• TopologicalSpace.setOf_isOpen_injective 📋 Mathlib.Topology.Order
  {α : Type u} : Function.Injective fun t => {s | IsOpen s}
• setOf_isOpen_iSup 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} : {s | IsOpen s} = ⋂ i, {s | IsOpen s}
• setOf_isOpen_sup 📋 Mathlib.Topology.Order
  {α : Type u} (t₁ t₂ : TopologicalSpace α) : {s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
• setOf_isOpen_sSup 📋 Mathlib.Topology.Order
  {α : Type u} {T : Set (TopologicalSpace α)} : {s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
• Topology.IsInducing.setOf_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) : {s | IsOpen s} = Set.preimage f '' {t | IsOpen t}
• Pairwise.countable_of_isOpen_disjoint 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (ho : ∀ (i : ι), IsOpen (s i)) (hne : ∀ (i : ι), (s i).Nonempty) : Countable ι
• TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : TopologicalSpace.IsTopologicalBasis s
• Set.PairwiseDisjoint.countable_of_isOpen 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i)) (hne : ∀ i ∈ a, (s i).Nonempty) : a.Countable
• subset_closure_inter_of_isPreirreducible_of_isOpen 📋 Mathlib.Topology.Irreducible
  {X : Type u_1} [TopologicalSpace X] {S U : Set X} (hS : IsPreirreducible S) (hU : IsOpen U) (h : (S ∩ U).Nonempty) : S ⊆ closure (S ∩ U)
• IsConnected.preimage_of_isOpenMap 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsConnected (f ⁻¹' s)
• IsPreconnected.preimage_of_isOpenMap 📋 Mathlib.Topology.Connected.Basic
  {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ Set.range f) : IsPreconnected (f ⁻¹' s)
• IsOpenQuotientMap.of_isOpenMap_isQuotientMap 📋 Mathlib.Topology.Maps.OpenQuotient
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ho : IsOpenMap f) (hq : Topology.IsQuotientMap f) : IsOpenQuotientMap f
• IsOpenQuotientMap.of_isOpenMap_quotientMap 📋 Mathlib.Topology.Maps.OpenQuotient
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (ho : IsOpenMap f) (hq : Topology.IsQuotientMap f) : IsOpenQuotientMap f
• IsCompact.closure_subset_of_isOpen 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K ⊆ U) : closure K ⊆ U
• exists_isOpen_singleton_of_isOpen_finite 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hfin : s.Finite) (hne : s.Nonempty) (ho : IsOpen s) : ∃ x ∈ s, IsOpen {x}
• discreteTopology_of_isOpen_singleton_one 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type w} [TopologicalSpace G] [Group G] [ContinuousMul G] (h : IsOpen {1}) : DiscreteTopology G
• discreteTopology_of_isOpen_singleton_zero 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type w} [TopologicalSpace G] [AddGroup G] [ContinuousAdd G] (h : IsOpen {0}) : DiscreteTopology G
• locPathConnected_of_isOpen 📋 Mathlib.Topology.Connected.PathConnected
  {X : Type u_1} [TopologicalSpace X] [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) : LocPathConnectedSpace ↑U
• TopCat.isIso_of_bijective_of_isOpenMap 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y : TopCat} (f : X ⟶ Y) (hfbij : Function.Bijective ⇑f) (hfcl : IsOpenMap ⇑f) : CategoryTheory.IsIso f
• isGδ_iInter_of_isOpen 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {f : ι' → Set X} (hf : ∀ (i : ι'), IsOpen (f i)) : IsGδ (⋂ i, f i)
• IsGδ.iInter_of_isOpen 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} {ι' : Sort u_4} [TopologicalSpace X] [Countable ι'] {f : ι' → Set X} (hf : ∀ (i : ι'), IsOpen (f i)) : IsGδ (⋂ i, f i)
• isGδ_biInter_of_isOpen 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {I : Set ι} (hI : I.Countable) {f : ι → Set X} (hf : ∀ i ∈ I, IsOpen (f i)) : IsGδ (⋂ i ∈ I, f i)
• IsGδ.biInter_of_isOpen 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] {I : Set ι} (hI : I.Countable) {f : ι → Set X} (hf : ∀ i ∈ I, IsOpen (f i)) : IsGδ (⋂ i ∈ I, f i)
• measurable_of_isOpen 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
  {γ : Type u_3} {δ : Type u_5} [TopologicalSpace γ] [MeasurableSpace γ] [BorelSpace γ] [MeasurableSpace δ] {f : δ → γ} (hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)) : Measurable f
• MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Regular
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop} [TopologicalSpace α] [μ.OuterRegular] (H : μ.InnerRegularWRT p IsOpen) (hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)) : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
• Convex.strictConvex_of_isOpen 📋 Mathlib.Analysis.Convex.Strict
  {𝕜 : Type u_1} {E : Type u_3} [OrderedSemiring 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : IsOpen s) (hs : Convex 𝕜 s) : StrictConvex 𝕜 s
• QuasiSeparatedSpace.of_isOpenEmbedding 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : Topology.IsOpenEmbedding f) [QuasiSeparatedSpace β] : QuasiSeparatedSpace α
• gauge_lt_one_of_mem_of_isOpen 📋 Mathlib.Analysis.Convex.Gauge
  {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs₂ : IsOpen s) {x : E} (hx : x ∈ s) : gauge s x < 1
• gauge_lt_one_eq_self_of_isOpen 📋 Mathlib.Analysis.Convex.Gauge
  {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs₁ : Convex ℝ s) (hs₀ : 0 ∈ s) (hs₂ : IsOpen s) : {x | gauge s x < 1} = s
• gaugeSeminorm_lt_one_of_isOpen 📋 Mathlib.Analysis.Convex.Gauge
  {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] {s : Set E} [RCLike 𝕜] [Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] {hs₀ : Balanced 𝕜 s} {hs₁ : Convex ℝ s} {hs₂ : Absorbent ℝ s} [TopologicalSpace E] [ContinuousSMul ℝ E] (hs : IsOpen s) {x : E} (hx : x ∈ s) : (gaugeSeminorm hs₀ hs₁ hs₂) x < 1
• MeasureTheory.Content.outerMeasure_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Content
  {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : Set G) (hU : IsOpen U) : μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }
• dense_iInter_of_isOpen_nat 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {f : ℕ → Set X} (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)) : Dense (⋂ n, f n)
• dense_iInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {ι : Sort u_3} [TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X} (ho : ∀ (i : ι), IsOpen (f i)) (hd : ∀ (i : ι), Dense (f i)) : Dense (⋂ s, f s)
• dense_sInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {S : Set (Set X)} (ho : ∀ s ∈ S, IsOpen s) (hS : S.Countable) (hd : ∀ s ∈ S, Dense s) : Dense (⋂₀ S)
• dense_biInter_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} {α : Type u_2} [TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X} (ho : ∀ s ∈ S, IsOpen (f s)) (hS : S.Countable) (hd : ∀ s ∈ S, Dense (f s)) : Dense (⋂ s ∈ S, f s)
• 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 ⇑f) (hF : F.IsSheaf) : TopCat.Presheaf.IsSheaf (⋯.functor.op.comp F)
• TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isOpenEmbedding 📋 Mathlib.Topology.Sheaves.Stalks
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑f) (F : TopCat.Presheaf C X) (x : ↑X) : CategoryTheory.IsIso (TopCat.Presheaf.stalkPushforward C f F x)
• AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} : AlgebraicGeometry.IsAffineOpen (f.opensFunctor.obj U) ↔ AlgebraicGeometry.IsAffineOpen U
• AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U)
• AlgebraicGeometry.isReduced_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Properties
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsReduced Y] : AlgebraicGeometry.IsReduced X
• AlgebraicGeometry.isIntegral_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Properties
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsIntegral Y] [Nonempty ↑↑X.toPresheafedSpace] : AlgebraicGeometry.IsIntegral X
• AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.FunctionField
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] [hX : IrreducibleSpace ↑↑X.toPresheafedSpace] [IrreducibleSpace ↑↑Y.toPresheafedSpace] : f.base (genericPoint ↑↑X.toPresheafedSpace) = genericPoint ↑↑Y.toPresheafedSpace
• AlgebraicGeometry.IsLocalAtSource.of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocalAtSource P] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [P.ContainsIdentities] [AlgebraicGeometry.IsOpenImmersion f] : P f
• AlgebraicGeometry.IsDominant.of_comp_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsDominant (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsOpenImmersion g] : AlgebraicGeometry.IsDominant f
• IsCompact.preimage_of_isOpen 📋 Mathlib.Topology.Spectral.Hom
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hf : IsSpectralMap f) (h₀ : IsCompact s) (h₁ : IsOpen s) : IsCompact (f ⁻¹' s)
• IsSpectralMap.isCompact_preimage_of_isOpen 📋 Mathlib.Topology.Spectral.Hom
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (self : IsSpectralMap f) ⦃s : Set β⦄ : IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)
• AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q) [AlgebraicGeometry.IsOpenImmersion f] : P f
• AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} [AlgebraicGeometry.HasRingHomProperty P Q] {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsOpenImmersion f] (H : P g) : P (CategoryTheory.CategoryStruct.comp f g)
• AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.FiniteType
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.LocallyOfFiniteType f
• AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective 📋 Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
  {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↑↑X.toPresheafedSpace] (hfopen : IsOpenMap ⇑f.base) (hfinj₁ : Function.Injective ⇑f.base) (hfinj₂ : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.app f ⊤)) (x : ↑↑X.toPresheafedSpace) : Function.Injective ⇑(AlgebraicGeometry.Scheme.Hom.stalkMap f x)
• AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] : AlgebraicGeometry.LocallyOfFinitePresentation f
• AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Noetherian
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsLocallyNoetherian Y] : AlgebraicGeometry.IsLocallyNoetherian X
• 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
• AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.SpreadingOut
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↑↑X.toPresheafedSpace} [AlgebraicGeometry.IsOpenImmersion f] : Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x
• fderivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (hs : IsOpen s) (hx : x ∈ s) : fderivWithin 𝕜 f s x = fderiv 𝕜 f x
• hasFDerivWithinAt_of_isOpen 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : IsOpen s) (hx : x ∈ s) : HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x
• derivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.Deriv.Basic
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x
• iteratedFDerivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (hs : IsOpen s) : Set.EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
• ContDiffOn.continuousOn_fderiv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Defs
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : ℕ∞} (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hn : 1 ≤ n) : ContinuousOn (fun x => fderiv 𝕜 f x) s
• contDiffOn_top_iff_fderiv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Defs
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (hs : IsOpen s) : ContDiffOn 𝕜 ⊤ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ⊤ (fun y => fderiv 𝕜 f y) s
• ContDiffOn.fderiv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Defs
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {m n : ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (fun y => fderiv 𝕜 f y) s
• contDiffOn_succ_iff_fderiv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Defs
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : ℕ} (hs : IsOpen s) : ContDiffOn 𝕜 (↑n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderiv 𝕜 f y) s
• AnalyticOnNhd.deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) : AnalyticOnNhd 𝕜 (deriv f) s
• AnalyticOnNhd.iteratedFDeriv_of_isOpen 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) (n : ℕ) : AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s
• AnalyticOnNhd.fderiv_of_isOpen 📋 Mathlib.Analysis.Calculus.FDeriv.Analytic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) : AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s
• ContDiffOn.continuousOn_deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (h : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hn : 1 ≤ n) : ContinuousOn (deriv f₂) s₂
• contDiffOn_top_iff_deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (hs : IsOpen s₂) : ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (deriv f₂) s₂
• ContDiffOn.deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (deriv f₂) s₂
• contDiffOn_succ_iff_deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₂ : 𝕜 → F} {s₂ : Set 𝕜} {n : ℕ} (hs : IsOpen s₂) : ContDiffOn 𝕜 (↑n + 1) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (deriv f₂) s₂
• Set.EqOn.iteratedDeriv_of_isOpen 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {f g : 𝕜 → F} (hfg : Set.EqOn f g s) (hs : IsOpen s) (n : ℕ) : Set.EqOn (iteratedDeriv n f) (iteratedDeriv n g) s
• WeakSpace.isOpen_of_isOpen 📋 Mathlib.Topology.Algebra.Module.WeakDual
  {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen (⇑(toWeakSpaceCLM 𝕜 E) '' V)) : IsOpen V
• exists_tsupport_one_of_isOpen_isClosed 📋 Mathlib.Topology.UrysohnsLemma
  {X : Type u_1} [TopologicalSpace X] [T2Space X] {s t : Set X} (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) : ∃ f, tsupport ⇑f ⊆ s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
• ContinuousMap.setOfIdeal_ofSet_of_isOpen 📋 Mathlib.Topology.ContinuousMap.Ideals
  {X : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] [TopologicalSpace X] [CompactSpace X] [T2Space X] {s : Set X} (hs : IsOpen s) : ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = s
• MeasureTheory.Measure.addHaarScalarFactor_pos_of_isOpenPosMeasure 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] : 0 < μ'.addHaarScalarFactor μ
• MeasureTheory.Measure.haarScalarFactor_pos_of_isOpenPosMeasure 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] : 0 < μ'.haarScalarFactor μ
• MeasureTheory.Measure.measure_isAddHaarMeasure_eq_smul_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [μ'.IsAddHaarMeasure] {s : Set G} (hs : IsOpen s) : μ' s = μ'.addHaarScalarFactor μ • μ s
• MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [μ'.IsHaarMeasure] {s : Set G} (hs : IsOpen s) : μ' s = μ'.haarScalarFactor μ • μ s
• lineDerivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.LineDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s : Set E} {x v : E} (hs : IsOpen s) (hx : x ∈ s) : lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v
• mfderivWithin_of_isOpen 📋 Mathlib.Geometry.Manifold.MFDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M} (hs : IsOpen s) (hx : x ∈ s) : mfderivWithin I I' f s x = mfderiv I I' f x
• exists_continuous_sum_one_of_isOpen_isCompact 📋 Mathlib.Topology.PartitionOfUnity
  {X : Type v} [TopologicalSpace X] [T2Space X] [LocallyCompactSpace X] {n : ℕ} {t : Set X} {s : Fin n → Set X} (hs : ∀ (i : Fin n), IsOpen (s i)) (htcp : IsCompact t) (hst : t ⊆ ⋃ i, s i) : ∃ f, (∀ (i : Fin n), tsupport ⇑(f i) ⊆ s i) ∧ Set.EqOn (∑ i : Fin n, ⇑(f i)) 1 t ∧ (∀ (i : Fin n) (x : X), (f i) x ∈ Set.Icc 0 1) ∧ ∀ (i : Fin n), HasCompactSupport ⇑(f i)
• VectorField.lieBracketWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.VectorField
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} (hs : IsOpen s) (hx : x ∈ s) : VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x
• cardinal_eq_of_isOpen 📋 Mathlib.Topology.Algebra.Module.Cardinality
  {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) : Cardinal.mk ↑s = Cardinal.mk E
• continuum_le_cardinal_of_isOpen 📋 Mathlib.Topology.Algebra.Module.Cardinality
  {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) : Cardinal.continuum ≤ Cardinal.mk ↑s
• AddSubgroup.isClosed_of_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : AddSubgroup G) (h : IsOpen ↑U) : IsClosed ↑U
• Subgroup.isClosed_of_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (h : IsOpen ↑U) : IsClosed ↑U
• AddSubgroup.quotient_finite_of_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] [CompactSpace G] (U : AddSubgroup G) (h : IsOpen ↑U) : Finite (G ⧸ U)
• Subgroup.quotient_finite_of_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] (U : Subgroup G) (h : IsOpen ↑U) : Finite (G ⧸ U)
• AddSubgroup.addSubgroupOf_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U K : AddSubgroup G) (h : IsOpen ↑K) : IsOpen ↑(K.addSubgroupOf U)
• Subgroup.subgroupOf_isOpen 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [Group G] [TopologicalSpace G] (U K : Subgroup G) (h : IsOpen ↑K) : IsOpen ↑(K.subgroupOf U)
• Ideal.isOpen_of_isOpen_subideal 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {R : Type u_1} [CommRing R] [TopologicalSpace R] [TopologicalRing R] {U I : Ideal R} (h : U ≤ I) (hU : IsOpen ↑U) : IsOpen ↑I
• AddSubgroup.quotient_finite_of_isOpen' 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] (U : AddSubgroup G) (K : AddSubgroup ↥U) (hUopen : IsOpen ↑U) (hKopen : IsOpen ↑K) : Finite (↥U ⧸ K)
• Subgroup.quotient_finite_of_isOpen' 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] (U : Subgroup G) (K : Subgroup ↥U) (hUopen : IsOpen ↑U) (hKopen : IsOpen ↑K) : Finite (↥U ⧸ K)
• CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen 📋 Mathlib.CategoryTheory.Galois.Topology
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {H : Set (CategoryTheory.Aut F)} (h1 : 1 ∈ H) (h : IsOpen H) : ∃ I x, (∀ X ∈ I, CategoryTheory.PreGaloisCategory.IsConnected X) ∧ ∀ (σ : CategoryTheory.Aut F), (∀ (X : ↑I), σ.hom.app ↑X = CategoryTheory.CategoryStruct.id (F.obj ↑X)) → σ ∈ H
• image_subset_closure_compl_image_compl_of_isOpen 📋 Mathlib.Topology.ExtremallyDisconnected
  {A E : Type u} [TopologicalSpace A] [TopologicalSpace E] {ρ : E → A} (ρ_cont : Continuous ρ) (ρ_surj : Function.Surjective ρ) (zorn_subset : ∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) {G : Set E} (hG : IsOpen G) : ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
• compactlyGeneratedSpace_of_isOpen 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X
• compactlyGeneratedSpace_of_isOpen_of_t2 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] [T2Space X] (h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X
• uCompactlyGeneratedSpace_of_isOpen 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type w} [tX : TopologicalSpace X] (h : ∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)) → IsOpen s) : UCompactlyGeneratedSpace X
• eventually_mapsTo_of_isOpen_of_omegaLimit_subset 📋 Mathlib.Dynamics.OmegaLimit
  {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [CompactSpace β] {v : Set β} (hv₁ : IsOpen v) (hv₂ : omegaLimit f ϕ s ⊆ v) : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s v
• eventually_mapsTo_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset 📋 Mathlib.Dynamics.OmegaLimit
  {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [T2Space β] {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s n
• eventually_closure_subset_of_isOpen_of_omegaLimit_subset 📋 Mathlib.Dynamics.OmegaLimit
  {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [CompactSpace β] {v : Set β} (hv₁ : IsOpen v) (hv₂ : omegaLimit f ϕ s ⊆ v) : ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ v
• eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset 📋 Mathlib.Dynamics.OmegaLimit
  {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) [T2Space β] {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∀ᶠ (t : τ) in f, Set.MapsTo (ϕ t) s c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
• eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' 📋 Mathlib.Dynamics.OmegaLimit
  {τ : Type u_1} {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α) {c : Set β} (hc₁ : IsCompact c) (hc₂ : ∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c) {n : Set β} (hn₁ : IsOpen n) (hn₂ : omegaLimit f ϕ s ⊆ n) : ∃ u ∈ f, closure (Set.image2 ϕ u s) ⊆ n
• tendsto_residual_of_isOpenMap 📋 Mathlib.Topology.Baire.BaireMeasurable
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hc : Continuous f) (ho : IsOpenMap f) : Filter.Tendsto f (residual α) (residual β)
• IsMeagre.preimage_of_isOpenMap 📋 Mathlib.Topology.Baire.BaireMeasurable
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hc : Continuous f) (ho : IsOpenMap f) {s : Set β} (h : IsMeagre s) : IsMeagre (f ⁻¹' s)
• Topology.IsLower.isLowerSet_of_isOpen 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} (h : IsOpen s) : IsLowerSet s
• Topology.IsUpper.isUpperSet_of_isOpen 📋 Mathlib.Topology.Order.LowerUpperTopology
  {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] {s : Set α} (h : IsOpen s) : IsUpperSet s
• Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen 📋 Mathlib.Topology.Order.ScottTopology
  {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s
• Topology.IsScott.isUpperSet_of_isOpen 📋 Mathlib.Topology.Order.ScottTopology
  {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α D] : IsOpen s → IsUpperSet s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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, _ * _, _ ^ _, |- _ < _ → _
woould 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.

This is Loogle revision 4e1aab0 serving mathlib revision b513113