Loogle!

Result

Found 179 declarations whose name contains "of_isOpen".

• Dense.inter_of_isOpen_left 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)
• Dense.inter_of_isOpen_right 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)
• DenseRange.subset_closure_image_preimage_of_isOpen 📋 Mathlib.Topology.Continuous
  {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}
• SeparatedNhds.isOpen_left_of_isOpen_union 📋 Mathlib.Topology.Separation.SeparatedNhds
  {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen s
• SeparatedNhds.isOpen_right_of_isOpen_union 📋 Mathlib.Topology.Separation.SeparatedNhds
  {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen t
• ContinuousOn.iUnion_of_isOpen 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hf : ∀ (i : ι), ContinuousOn f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : ContinuousOn f (⋃ i, s i)
• continuousOn_iUnion_iff_of_isOpen 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hs : ∀ (i : ι), IsOpen (s i)) : ContinuousOn f (⋃ i, s i) ↔ ∀ (i : ι), ContinuousOn f (s i)
• continuous_of_continuousOn_iUnion_of_isOpen 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hf : ∀ (i : ι), ContinuousOn f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ i, s i = Set.univ) : Continuous f
• ContinuousOn.union_of_isOpen 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hfs : ContinuousOn f s) (hft : ContinuousOn f t) (hs : IsOpen s) (ht : IsOpen t) : ContinuousOn f (s ∪ t)
• continouousOn_union_iff_of_isOpen 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hs : IsOpen s) (ht : IsOpen t) : ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t
• TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : TopologicalSpace.IsTopologicalBasis s) (hss' : s ⊆ s') : TopologicalSpace.IsTopologicalBasis s'
• Pairwise.countable_of_isOpen_disjoint 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} (hd : Pairwise (Function.onFun Disjoint 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
• TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : TopologicalSpace.IsTopologicalBasis t✝) {u : Set α} (hu : IsOpen u) : ∃ s ⊆ t✝, s.Countable ∧ u = ⋃ a ∈ s, a
• 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)
• 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
• isEmbedding_of_isOpenQuotientMap_of_isInducing 📋 Mathlib.Topology.Maps.OpenQuotient
  {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D) (h : g ∘ p = q ∘ f) (hf : Topology.IsInducing f) (hp : Topology.IsQuotientMap p) (hq : IsOpenQuotientMap q) (hg : Function.Injective g) (H : q ⁻¹' (q '' Set.range f) ⊆ Set.range f) : Topology.IsEmbedding g
• isQuotientMap_of_isOpenQuotientMap_of_isInducing 📋 Mathlib.Topology.Maps.OpenQuotient
  {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D) (h : g ∘ p = q ∘ f) (hf : Topology.IsInducing f) (hp : Function.Surjective p) (hq : IsOpenQuotientMap q) (hg : Topology.IsEmbedding g) (H : q ⁻¹' (q '' Set.range f) ⊆ Set.range f) : Topology.IsQuotientMap p
• coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing 📋 Mathlib.Topology.Maps.OpenQuotient
  {A : Type u_4} {B : Type u_5} {C : Type u_6} {D : Type u_7} [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace D] (f : A → B) (g : C → D) (p : A → C) (q : B → D) (h : g ∘ p = q ∘ f) (hf : Topology.IsInducing f) (hp : Function.Surjective p) (hq : IsOpenQuotientMap q) (hg : Function.Injective g) (H : q ⁻¹' (q '' Set.range f) ⊆ Set.range f) : TopologicalSpace.coinduced p inst✝ = TopologicalSpace.induced g inst✝¹
• 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
• eventually_nhdsWithin_eventually_nhds_iff_of_isOpen 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} {a : X} {p : X → Prop} (hs : IsOpen s) : (∀ᶠ (y : X) in nhdsWithin a s, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhdsWithin a s, p x
• 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}
• t2Space_iff_of_isOpenQuotientMap 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {π : X → Y} (h : IsOpenQuotientMap π) : T2Space Y ↔ IsClosed {q | π q.1 = π q.2}
• 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)
• 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
• TopCat.isIso_of_bijective_of_isOpenMap 📋 Mathlib.Topology.Category.TopCat.Basic
  {X Y : TopCat} (f : X ⟶ Y) (hfbij : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)) (hfcl : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso f
• CompactlyCoherentSpace.of_isOpen_forall_compactSpace 📋 Mathlib.Topology.Compactness.CompactlyCoherentSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ (s : Set X), (∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] (f : K → X), Continuous f → IsOpen (f ⁻¹' s)) → IsOpen s) : CompactlyCoherentSpace X
• CompactlyCoherentSpace.of_isOpen 📋 Mathlib.Topology.Compactness.CompactlyCoherentSpace
  {X : Type u} [TopologicalSpace X] (h : ∀ (A : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' A)) → IsOpen A) : CompactlyCoherentSpace X
• IsDiscrete.image_of_isOpenMap 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hs : IsDiscrete s) (hf : IsOpenMap f) (hf' : Function.Injective f) : IsDiscrete (f '' s)
• IsDiscrete.image_of_isOpenMap_of_isOpen 📋 Mathlib.Topology.DiscreteSubset
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hs : IsDiscrete s) (hf : IsOpenMap f) (hs' : IsOpen s) : IsDiscrete (f '' s)
• QuasiSeparatedSpace.of_isOpenEmbedding 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [QuasiSeparatedSpace α] {f : β → α} (h : Topology.IsOpenEmbedding f) : QuasiSeparatedSpace β
• IsCompact.inter_of_isOpen 📋 Mathlib.Topology.QuasiSeparated
  {α : Type u_1} [TopologicalSpace α] [QuasiSeparatedSpace α] {U V : Set α} (hUcomp : IsCompact U) (hVcomp : IsCompact V) (hUopen : IsOpen U) (hVopen : IsOpen V) : IsCompact (U ∩ V)
• 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)
• PrespectralSpace.of_isOpenCover 📋 Mathlib.Topology.Spectral.Prespectral
  {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) [∀ (i : ι), PrespectralSpace ↥(U i)] : 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.IsLocallyConstructible.inter_of_isOpen_isCompact 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s t : Set X} [PrespectralSpace X] [QuasiSeparatedSpace X] (hs : Topology.IsLocallyConstructible s) (ht : IsOpen t) (ht' : IsCompact t) : Topology.IsConstructible (s ∩ t)
• Topology.IsLocallyConstructible.of_isOpenCover' 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) (H : ∀ (i : ι), Topology.IsLocallyConstructible (s ∩ ↑(U i))) : Topology.IsLocallyConstructible s
• QuasiSeparatedSpace.of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) (h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)) (h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)) : QuasiSeparatedSpace X
• 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.IsLocallyConstructible.iff_isConstructible_of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} [PrespectralSpace X] [QuasiSeparatedSpace X] (hU : TopologicalSpace.IsOpenCover U) (hU' : ∀ (i : ι), IsCompact ↑(U i)) : Topology.IsLocallyConstructible s ↔ ∀ (i : ι), Topology.IsConstructible (s ∩ ↑(U i))
• Topology.IsLocallyConstructible.of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) (H : ∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s)) : Topology.IsLocallyConstructible s
• Topology.IsLocallyConstructible.iff_of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) : Topology.IsLocallyConstructible s ↔ ∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s)
• PrimeSpectrum.eq_biUnion_of_isOpen 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} [CommSemiring R] {s : Set (PrimeSpectrum R)} (hs : IsOpen s) : s = ⋃ r, ⋃ (_ : ↑(PrimeSpectrum.basicOpen r) ⊆ s), ↑(PrimeSpectrum.basicOpen r)
• 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)
• 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} [Semiring 𝕜] [PartialOrder 𝕜] [TopologicalSpace E] [AddCommMonoid E] [Module 𝕜 E] {s : Set E} (h : IsOpen s) (hs : Convex 𝕜 s) : StrictConvex 𝕜 s
• 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 }
• not_isMeagre_of_isOpen 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {s : Set X} (hs : IsOpen s) (hne : s.Nonempty) : ¬IsMeagre s
• dense_iInter_of_isOpen_nat 📋 Mathlib.Topology.Baire.Lemmas
  {X : Type u_1} [TopologicalSpace X] [BaireSpace X] {f : ℕ → Set X} (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)) : Dense (⋂ n, f n)
• 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 ⇑(CategoryTheory.ConcreteCategory.hom f)) (hF : F.IsSheaf) : TopCat.Presheaf.IsSheaf (⋯.functor.op.comp F)
• AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top 📋 Mathlib.AlgebraicGeometry.OpenImmersion
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (hf : AlgebraicGeometry.Scheme.Hom.opensRange f = ⊤) : CategoryTheory.IsIso f
• 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.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens} : AlgebraicGeometry.IsAffineOpen ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) ↔ AlgebraicGeometry.IsAffineOpen U
• AlgebraicGeometry.IsAffineOpen.preimage_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X Y : AlgebraicGeometry.Scheme} {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (hU' : U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f) : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
• AlgebraicGeometry.IsLocalAtSource.of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P] {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [P.ContainsIdentities] [AlgebraicGeometry.IsOpenImmersion f] : P f
• AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Morphisms.Basic
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource 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
• 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.Scheme.quasiSeparatedSpace_of_isOpenCover 📋 Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
  {X : AlgebraicGeometry.Scheme} {I : Type u_1} (U : I → X.Opens) (hU : TopologicalSpace.IsOpenCover U) (hU₁ : ∀ (i : I), AlgebraicGeometry.IsAffineOpen (U i)) (hU₂ : ∀ (i j : I), IsCompact (↑(U i) ∩ ↑(U j))) : QuasiSeparatedSpace ↥X
• AlgebraicGeometry.isReduced_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Properties
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsReduced Y] : AlgebraicGeometry.IsReduced X
• AlgebraicGeometry.isIntegral_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Properties
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsIntegral Y] [Nonempty ↥X] : AlgebraicGeometry.IsIntegral X
• AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Basic
  {X Y U V : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) [AlgebraicGeometry.IsOpenImmersion iV] [AlgebraicGeometry.QuasiCompact f] (H : CategoryTheory.IsPullback f' iU iV f) (W : ↑V.affineOpens) : (AlgebraicGeometry.Scheme.Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso iV ↑W).inv) ((AlgebraicGeometry.Scheme.Hom.ker f).ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor iV).obj ↑W, ⋯⟩)
• 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.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] (hfopen : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (hfinj₁ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (hfinj₂ : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))) (x : ↥X) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (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.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] (U : ↑X.affineOpens) : (I.comap f).ideal U = Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso f ↑U).inv) (I.ideal ⟨(AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑U, ⋯⟩)
• 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] [IsTopologicalRing 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] [IsTopologicalAddGroup 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] [IsTopologicalGroup G] [CompactSpace G] (U : Subgroup G) (K : Subgroup ↥U) (hUopen : IsOpen ↑U) (hKopen : IsOpen ↑K) : Finite (↥U ⧸ K)
• AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.FunctionField
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [hX : IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] : (CategoryTheory.ConcreteCategory.hom f.base) (genericPoint ↥X) = genericPoint ↥Y
• AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.Noetherian
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.IsLocallyNoetherian Y] : AlgebraicGeometry.IsLocallyNoetherian X
• AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion 📋 Mathlib.AlgebraicGeometry.SpreadingOut
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} [AlgebraicGeometry.IsOpenImmersion f] : Y.IsGermInjectiveAt ((CategoryTheory.ConcreteCategory.hom f.base) x) ↔ X.IsGermInjectiveAt x
• DifferentiableOn.iUnion_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} {ι : Type u_4} {s : ι → Set E} (hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : DifferentiableOn 𝕜 f (⋃ i, s i)
• differentiableOn_iUnion_iff_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} {ι : Type u_4} {s : ι → Set E} (hs : ∀ (i : ι), IsOpen (s i)) : DifferentiableOn 𝕜 f (⋃ i, s i) ↔ ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
• differentiable_of_differentiableOn_iUnion_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} {ι : Type u_4} {s : ι → Set E} (hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ i, s i = Set.univ) : Differentiable 𝕜 f
• DifferentiableOn.union_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} {s t : Set E} (hf : DifferentiableOn 𝕜 f s) (hf' : DifferentiableOn 𝕜 f t) (hs : IsOpen s) (ht : IsOpen t) : DifferentiableOn 𝕜 f (s ∪ t)
• differentiableOn_union_iff_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} {s t : Set E} (hs : IsOpen s) (ht : IsOpen t) : DifferentiableOn 𝕜 f (s ∪ t) ↔ DifferentiableOn 𝕜 f s ∧ DifferentiableOn 𝕜 f t
• differentiable_of_differentiableOn_union_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} {s t : Set E} (hf : DifferentiableOn 𝕜 f s) (hf' : DifferentiableOn 𝕜 f t) (hst : s ∪ t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) : Differentiable 𝕜 f
• 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
• 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_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 : WithTop ℕ∞} (h : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hn : 1 ≤ n) : ContinuousOn (fderiv 𝕜 f) s
• contDiffOn_infty_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 𝕜 (↑⊤) (fderiv 𝕜 f) 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 : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hs : IsOpen s) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (fderiv 𝕜 f) 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 : WithTop ℕ∞} (hs : IsOpen s) : ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) s
• iteratedDerivWithin_of_isOpen 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDeriv n f) s
• iteratedDerivWithin_of_isOpen_eq_iterate 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} (hs : IsOpen s) : Set.EqOn (iteratedDerivWithin n f s) (deriv^[n] f) s
• iteratedDerivWithin_congr_right_of_isOpen 📋 Mathlib.Analysis.Calculus.IteratedDeriv.Defs
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : 𝕜 → F) (n : ℕ) {s t : Set 𝕜} (hs : IsOpen s) (ht : IsOpen t) : Set.EqOn (iteratedDerivWithin n f s) (iteratedDerivWithin n f t) (s ∩ t)
• cardinal_eq_of_isOpen 📋 Mathlib.Topology.Algebra.Module.Cardinality
  {E : Type u_1} (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] [AddGroup E] [MulActionWithZero 𝕜 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
• ContDiffOn.iUnion_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_3} {s : ι → Set E} (hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : ContDiffOn 𝕜 n f (⋃ i, s i)
• contDiffOn_iUnion_iff_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_3} {s : ι → Set E} (hs : ∀ (i : ι), IsOpen (s i)) : ContDiffOn 𝕜 n f (⋃ i, s i) ↔ ∀ (i : ι), ContDiffOn 𝕜 n f (s i)
• contDiff_of_contDiffOn_iUnion_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_3} {s : ι → Set E} (hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ i, s i = Set.univ) : ContDiff 𝕜 n f
• ContDiffOn.union_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hs : IsOpen s) (ht : IsOpen t) : ContDiffOn 𝕜 n f (s ∪ t)
• contDiffOn_union_iff_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hs : IsOpen s) (ht : IsOpen t) : ContDiffOn 𝕜 n f (s ∪ t) ↔ ContDiffOn 𝕜 n f s ∧ ContDiffOn 𝕜 n f t
• contDiff_of_contDiffOn_union_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hst : s ∪ t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) : ContDiff 𝕜 n f
• ContDiffOn.continuousOn_deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (h : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hn : 1 ≤ n) : ContinuousOn (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 : WithTop ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : IsOpen s₂) (hmn : m + 1 ≤ n) : ContDiffOn 𝕜 m (deriv f₂) s₂
• contDiffOn_infty_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_succ_iff_deriv_of_isOpen 📋 Mathlib.Analysis.Calculus.ContDiff.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f₂ : 𝕜 → F} {s₂ : Set 𝕜} (hs : IsOpen s₂) : ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ⊤ → AnalyticOn 𝕜 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
• 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
• 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] [R1Space 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.measure_isAddHaarMeasure_eq_smul_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Haar.Unique
  {G : Type u_1} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup 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] [IsTopologicalGroup 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
• ContMDiffOn.iUnion_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M} (hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : ContMDiffOn I I' n f (⋃ i, s i)
• contMDiffOn_iUnion_iff_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M} (hs : ∀ (i : ι), IsOpen (s i)) : ContMDiffOn I I' n f (⋃ i, s i) ↔ ∀ (i : ι), ContMDiffOn I I' n f (s i)
• contMDiff_of_contMDiffOn_iUnion_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {ι : Type u_11} {s : ι → Set M} (hf : ∀ (i : ι), ContMDiffOn I I' n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ i, s i = Set.univ) : ContMDiff I I' n f
• ContMDiffOn.union_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {s t : Set M} (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t) (hs : IsOpen s) (ht : IsOpen t) : ContMDiffOn I I' n f (s ∪ t)
• contMDiffOn_union_iff_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {s t : Set M} (hs : IsOpen s) (ht : IsOpen t) : ContMDiffOn I I' n f (s ∪ t) ↔ ContMDiffOn I I' n f s ∧ ContMDiffOn I I' n f t
• contMDiff_of_contMDiffOn_union_of_isOpen 📋 Mathlib.Geometry.Manifold.ContMDiff.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] {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] [ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞} {s t : Set M} (hf : ContMDiffOn I I' n f s) (hf' : ContMDiffOn I I' n f t) (hst : s ∪ t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) : ContMDiff I I' n f
• MDifferentiableOn.iUnion_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'} {ι : Type u_11} {s : ι → Set M} (hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : MDifferentiableOn I I' f (⋃ i, s i)
• mdifferentiableOn_iUnion_iff_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'} {ι : Type u_11} {s : ι → Set M} (hs : ∀ (i : ι), IsOpen (s i)) : MDifferentiableOn I I' f (⋃ i, s i) ↔ ∀ (i : ι), MDifferentiableOn I I' f (s i)
• mdifferentiable_of_mdifferentiableOn_iUnion_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'} {ι : Type u_11} {s : ι → Set M} (hf : ∀ (i : ι), MDifferentiableOn I I' f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ i, s i = Set.univ) : MDifferentiable I I' f
• MDifferentiableOn.union_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'} {s t : Set M} (hf : MDifferentiableOn I I' f s) (hf' : MDifferentiableOn I I' f t) (hs : IsOpen s) (ht : IsOpen t) : MDifferentiableOn I I' f (s ∪ t)
• mdifferentiableOn_union_iff_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'} {s t : Set M} (hs : IsOpen s) (ht : IsOpen t) : MDifferentiableOn I I' f (s ∪ t) ↔ MDifferentiableOn I I' f s ∧ MDifferentiableOn I I' f t
• mdifferentiable_of_mdifferentiableOn_union_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'} {s t : Set M} (hf : MDifferentiableOn I I' f s) (hf' : MDifferentiableOn I I' f t) (hst : s ∪ t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) : MDifferentiable I I' f
• 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, ⇑(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
• 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] [CompactSpace K] [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
• VectorField.mlieBracketWithin_of_isOpen 📋 Mathlib.Geometry.Manifold.VectorField.LieBracket
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x} (hs : IsOpen s) (hx : x ∈ s) : VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracket I V W x
• MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [SecondCountableTopology Ω] {S : Set (Set Ω)} (ν : MeasureTheory.ProbabilityMeasure Ω) (h : ∀ (u : Set Ω), IsOpen u → ∀ x ∈ u, ∃ s ∈ S, s ∈ nhds x ∧ s ⊆ u) {G : Set Ω} (hG : IsOpen G) {r : NNReal} (hr : r < ν G) : ∃ T, (∀ t ∈ T, t ∈ S) ∧ r < ν (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
• MeasureTheory.Measure.subset_compl_support_of_isOpen 📋 Mathlib.MeasureTheory.Measure.Support
  {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {t : Set X} (ht : IsOpen t) (h : μ t = 0) : t ⊆ μ.supportᶜ
• 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)
• UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen 📋 Mathlib.Topology.UniformSpace.Closeds
  {α : Type u_1} [UniformSpace α] {U : Set α} (hU : IsOpen U) : IsOpen {s | (s ∩ U).Nonempty}
• TopologicalSpace.Closeds.isOpen_inter_nonempty_of_isOpen 📋 Mathlib.Topology.UniformSpace.Closeds
  {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) : IsOpen {t | (↑t ∩ s).Nonempty}
• TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen 📋 Mathlib.Topology.UniformSpace.Closeds
  {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) : IsOpen {t | (↑t ∩ s).Nonempty}
• TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen 📋 Mathlib.Topology.UniformSpace.Closeds
  {α : Type u_1} [UniformSpace α] {s : Set α} (hs : IsOpen s) : IsOpen {t | (↑t ∩ s).Nonempty}
• 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
• IsCompactOpenCovered.of_isOpenMap 📋 Mathlib.Topology.Sets.CompactOpenCovered
  {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] [TopologicalSpace S] [∀ (i : ι), PrespectralSpace (X i)] (hfc : ∀ (i : ι), Continuous (f i)) (h : ∀ (i : ι), IsOpenMap (f i)) {U : Set S} (hs : ∀ x ∈ U, ∃ i y, f i y = x) (hU : IsOpen U) (hc : IsCompact U) : IsCompactOpenCovered f U

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

This is Loogle revision 6ff4759 serving mathlib revision f91c049