Loogle!

Result

Found 1689 declarations mentioning IsOpen. Of these, only the first 200 are shown.

• IsOpen 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] : Set X → Prop
• isOpen_univ 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] : IsOpen Set.univ
• IsClosed.isOpen_compl 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} {inst✝ : TopologicalSpace X} {s : Set X} [self : IsClosed s] : IsOpen sᶜ
• IsClosed.mk 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] {s : Set X} (isOpen_compl : IsOpen sᶜ) : IsClosed s
• IsOpen.inter 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ t)
• Continuous.isOpen_preimage 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (self : Continuous f) (s : Set Y) : IsOpen s → IsOpen (f ⁻¹' s)
• Continuous.mk 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (isOpen_preimage : ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)) : Continuous f
• isOpen_sUnion 📋 Mathlib.Topology.Defs.Basic
  {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋃₀ s)
• BaireSpace.baire_property 📋 Mathlib.Topology.Defs.Basic
  {X : Type u_1} {inst✝ : TopologicalSpace X} [self : BaireSpace X] (f : ℕ → Set X) : (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)
• BaireSpace.mk 📋 Mathlib.Topology.Defs.Basic
  {X : Type u_1} [TopologicalSpace X] (baire_property : ∀ (f : ℕ → Set X), (∀ (n : ℕ), IsOpen (f n)) → (∀ (n : ℕ), Dense (f n)) → Dense (⋂ n, f n)) : BaireSpace X
• nhds_def 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (x : X) : nhds x = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal s
• isOpen_const 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {p : Prop} : IsOpen {_x | p}
• isOpen_empty 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] : IsOpen ∅
• IsOpen.isLocallyClosed 📋 Mathlib.Topology.Basic
  {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) : IsLocallyClosed s
• isOpen_fold 📋 Mathlib.Topology.Basic
  {X : Type u} {s : Set X} {t : TopologicalSpace X} : TopologicalSpace.IsOpen s = IsOpen s
• IsOpen.isClosed_compl 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s → IsClosed sᶜ
• isClosed_compl_iff 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed sᶜ ↔ IsOpen s
• isOpen_compl_iff 📋 Mathlib.Topology.Basic
  {X : Type u} {s : Set X} [TopologicalSpace X] : IsOpen sᶜ ↔ IsClosed s
• TopologicalSpace.ext 📋 Mathlib.Topology.Basic
  {X : Type u} {f g : TopologicalSpace X} : IsOpen = IsOpen → f = g
• isOpen_iUnion 📋 Mathlib.Topology.Basic
  {X : Type u} {ι : Sort v} [TopologicalSpace X] {f : ι → Set X} (h : ∀ (i : ι), IsOpen (f i)) : IsOpen (⋃ i, f i)
• IsClosed.not 📋 Mathlib.Topology.Basic
  {X : Type u} {p : X → Prop} [TopologicalSpace X] : IsClosed {a | p a} → IsOpen {a | ¬p a}
• TopologicalSpace.ext_iff 📋 Mathlib.Topology.Basic
  {X : Type u} {t t' : TopologicalSpace X} : t = t' ↔ ∀ (s : Set X), IsOpen s ↔ IsOpen s
• isOpen_iInter_of_finite 📋 Mathlib.Topology.Basic
  {X : Type u} {ι : Sort v} [TopologicalSpace X] [Finite ι] {s : ι → Set X} (h : ∀ (i : ι), IsOpen (s i)) : IsOpen (⋂ i, s i)
• IsClosed.sdiff 📋 Mathlib.Topology.Basic
  {X : Type u} {s t : Set X} [TopologicalSpace X] (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t)
• IsOpen.sdiff 📋 Mathlib.Topology.Basic
  {X : Type u} {s t : Set X} [TopologicalSpace X] (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t)
• IsOpen.union 📋 Mathlib.Topology.Basic
  {X : Type u} {s₁ s₂ : Set X} [TopologicalSpace X] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂)
• isClosed_imp 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {p q : X → Prop} (hp : IsOpen {x | p x}) (hq : IsClosed {x | q x}) : IsClosed {x | p x → q x}
• Set.Finite.isOpen_sInter 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (hs : s.Finite) (h : ∀ t ∈ s, IsOpen t) : IsOpen (⋂₀ s)
• IsOpen.and 📋 Mathlib.Topology.Basic
  {X : Type u} {p₁ p₂ : X → Prop} [TopologicalSpace X] : IsOpen {x | p₁ x} → IsOpen {x | p₂ x} → IsOpen {x | p₁ x ∧ p₂ x}
• IsOpen.iInter_of_finite_ne_univ 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {ι : Type u_2} {s : ι → Set X} (hs : ∀ (i : ι), IsOpen (s i)) (hs_ne_univ : {i | s i ≠ Set.univ}.Finite) : IsOpen (⋂ i, s i)
• isOpen_iff_of_cover 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} {s : Set X} [TopologicalSpace X] {f : α → Set X} (ho : ∀ (i : α), IsOpen (f i)) (hU : ⋃ i, f i = Set.univ) : IsOpen s ↔ ∀ (i : α), IsOpen (f i ∩ s)
• isOpen_biUnion 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋃ i ∈ s, f i)
• Set.Finite.isOpen_biInter 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Set α} {f : α → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)
• isOpen_mk 📋 Mathlib.Topology.Basic
  {X : Type u} {s : Set X} {p : Set X → Prop} {h₁ : p Set.univ} {h₂ : ∀ (s t : Set X), p s → p t → p (s ∩ t)} {h₃ : ∀ (s : Set (Set X)), (∀ t ∈ s, p t) → p (⋃₀ s)} : IsOpen s ↔ p s
• isOpen_biInter_finset 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i)
• isOpen_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen (interior s)
• IsOpen.interior_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : IsOpen s) : interior s = s
• interior_eq_iff_isOpen 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = s ↔ IsOpen s
• subset_interior_iff_isOpen 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : s ⊆ interior s ↔ IsOpen s
• forall_isOpen_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {p : Set X → Prop} : (∀ (t : Set X), IsOpen t → p t) ↔ ∀ (t : Set X), p (interior t)
• IsOpen.subset_interior_closure 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (s_open : IsOpen s) : s ⊆ interior (closure s)
• IsOpen.frontier_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : frontier s = closure s \ s
• Dense.inter_open_nonempty 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
• IsOpen.inter_frontier_eq 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : s ∩ frontier s = ∅
• dense_iff_inter_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
• interior_maximal 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s
• exists_isOpen_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {p : Set X → Prop} : (∃ t, IsOpen t ∧ p t) ↔ ∃ t, p (interior t)
• IsOpen.subset_interior_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t
• dense_compl_singleton_iff_not_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {x : X} : Dense {x}ᶜ ↔ ¬IsOpen {x}
• closure_inter_open_nonempty_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen t) : (closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty
• Filter.HasBasis.lift'_interior_eq_self 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) (ho : ∀ (i : ι), p i → IsOpen (s i)) : l.lift' interior = l
• interior_subset_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} : interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t
• Dense.exists_mem_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) : ∃ x ∈ s, x ∈ U
• mem_closure_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
• subset_interior_iff 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
• mem_interior 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
• isOpen_iff_forall_mem_open 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
• disjoint_frontier_iff_isOpen 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s : Set X} : Disjoint (frontier s) s ↔ IsOpen s
• Disjoint.closure_left 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (ht : IsOpen t) : Disjoint (closure s) t
• Disjoint.closure_right 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hd : Disjoint s t) (hs : IsOpen s) : Disjoint s (closure t)
• Disjoint.frontier_left 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) (hd : Disjoint s t) : Disjoint (frontier s) t
• Disjoint.frontier_right 📋 Mathlib.Topology.Closure
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) (hd : Disjoint s t) : Disjoint s (frontier t)
• isOpen_setOfPred_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• isOpen_setOf_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• isOpen_singleton_iff_nhds_eq_pure 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhds x = pure x
• 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)
• nhds_basis_opens 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
• IsOpen.mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : s ∈ nhds x
• isOpen_iff_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x
• Dense.open_subset_closure_inter 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s)
• IsOpen.mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) : s ∈ nhds x ↔ x ∈ s
• IsOpen.eventually_mem 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ (x : X) in nhds x, x ∈ s
• isOpen_iff_eventually 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s
• nhds_basis_opens' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsOpen s) fun x => x
• IsOpen.closure_inter 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t)
• IsOpen.inter_closure 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t)
• isOpen_iff_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s
• isOpen_singleton_iff_punctured_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥
• frequently_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∃ᶠ (y : X) in nhds x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y
• mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
• eventually_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
• le_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} : f ≤ nhds x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f
• tendsto_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} : Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l
• nhds_le_of_le 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} {f : Filter X} (h : x ∈ s) (o : IsOpen s) (sf : Filter.principal s ≤ f) : nhds x ≤ f
• exists_open_set_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s U : Set X} (h : ∀ x ∈ s, U ∈ nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
• all_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) (P : Set X → Prop) (hP : ∀ (s t : Set X), s ⊆ t → P s → P t) : (∀ s ∈ nhds x, P s) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s
• nhds_def' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : nhds x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal s
• tendsto_atTop_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [Nonempty α] [SemilatticeSup α] {f : α → X} : Filter.Tendsto f Filter.atTop (nhds x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U
• exists_open_set_nhds' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s U : Set X} (h : U ∈ ⨆ x ∈ s, nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
• all_mem_nhds_filter 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} (x : X) (f : Set X → Set α) (hf : ∀ (s t : Set X), s ⊆ t → f s ⊆ f t) (l : Filter α) : (∀ s ∈ nhds x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l
• map_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : X → α} : Filter.map f (nhds x) = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)
• not_isOpen_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : ¬IsOpen {x}
• IsOpen.preimage 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {t : Set Y} (h : IsOpen t) : IsOpen (f ⁻¹' t)
• continuous_def 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} {x✝ : TopologicalSpace X} {x✝¹ : TopologicalSpace Y} {f : X → Y} : Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
• DenseRange.exists_mem_open 📋 Mathlib.Topology.Continuous
  {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X} (hf : DenseRange f) (ho : IsOpen s) (hs : s.Nonempty) : ∃ a, f a ∈ s
• 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)
• Topology.IsOpenEmbedding.isOpen_range 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (self : Topology.IsOpenEmbedding f) : IsOpen (Set.range f)
• Topology.IsOpenEmbedding.mk 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y} (toIsEmbedding : Topology.IsEmbedding f) (isOpen_range : IsOpen (Set.range f)) : Topology.IsOpenEmbedding f
• Topology.isOpenEmbedding_iff 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y) : Topology.IsOpenEmbedding f ↔ Topology.IsEmbedding f ∧ IsOpen (Set.range f)
• Topology.IsCoherentWith.isOpen_of_forall_induced 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (self : Topology.IsCoherentWith S) (u : Set X) : (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u
• Topology.IsCoherentWith.mk 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (isOpen_of_forall_induced : ∀ (u : Set X), (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u) : Topology.IsCoherentWith S
• isOpen_singleton_true 📋 Mathlib.Topology.Order
  : IsOpen {True}
• isOpen_discrete 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) : IsOpen s
• discreteTopology_iff_forall_isOpen 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (s : Set α), IsOpen s
• discreteTopology_iff_isOpen_singleton 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (a : α), IsOpen {a}
• TopologicalSpace.generateFrom_setOfPred_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} (t : TopologicalSpace α) : TopologicalSpace.generateFrom {s | IsOpen s} = t
• TopologicalSpace.generateFrom_setOf_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} (t : TopologicalSpace α) : TopologicalSpace.generateFrom {s | IsOpen s} = t
• TopologicalSpace.setOfPred_isOpen_injective 📋 Mathlib.Topology.Order
  {α : Type u} : Function.Injective fun t => {s | IsOpen s}
• TopologicalSpace.setOf_isOpen_injective 📋 Mathlib.Topology.Order
  {α : Type u} : Function.Injective fun t => {s | IsOpen s}
• continuous_Prop 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] {p : α → Prop} : Continuous p ↔ IsOpen {x | p x}
• TopologicalSpace.leftInverse_generateFrom 📋 Mathlib.Topology.Order
  {α : Type u} : Function.LeftInverse TopologicalSpace.generateFrom fun t => {s | IsOpen s}
• isOpen_singleton_nhdsAdjoint 📋 Mathlib.Topology.Order
  {α : Type u_1} {a b : α} (f : Filter α) (hb : b ≠ a) : IsOpen {b}
• TopologicalSpace.isOpen_generateFrom_of_mem 📋 Mathlib.Topology.Order
  {α : Type u} {g : Set (Set α)} {s : Set α} (hs : s ∈ g) : IsOpen s
• isOpen_iff_continuous_mem 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ Continuous fun x => x ∈ s
• isOpen_induced 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set β} (h : IsOpen s) : IsOpen (f ⁻¹' s)
• isOpen_coinduced 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β} : IsOpen s ↔ IsOpen (f ⁻¹' s)
• IsOpen.mono 📋 Mathlib.Topology.Order
  {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (hs : IsOpen s) (h : t₁ ≤ t₂) : IsOpen s
• isOpen_implies_isOpen_iff 📋 Mathlib.Topology.Order
  {α : Type u_1} {t₁ t₂ : TopologicalSpace α} : (∀ (s : Set α), IsOpen s → IsOpen s) ↔ t₂ ≤ t₁
• IndiscreteTopology.isOpen_iff 📋 Mathlib.Topology.Order
  {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] (U : Set α) : IsOpen U ↔ U = ∅ ∨ U = Set.univ
• continuous_discrete_rng 📋 Mathlib.Topology.Order
  {β : Type u_2} {α : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} : Continuous f ↔ ∀ (b : β), IsOpen (f ⁻¹' {b})
• isOpen_induced_iff 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β} : IsOpen s ↔ ∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = s
• isOpen_iSup_iff 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α} : IsOpen s ↔ ∀ (i : ι), IsOpen s
• le_generateFrom 📋 Mathlib.Topology.Order
  {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) : t ≤ TopologicalSpace.generateFrom g
• TopologicalSpace.le_def 📋 Mathlib.Topology.Order
  {α : Type u_1} {t s : TopologicalSpace α} : t ≤ s ↔ IsOpen ≤ IsOpen
• continuous_generateFrom_iff 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} {b : Set (Set β)} : Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
• isOpen_sup 📋 Mathlib.Topology.Order
  {α : Type u} {t₁ t₂ : TopologicalSpace α} {s : Set α} : IsOpen s ↔ IsOpen s ∧ IsOpen s
• TopologicalSpace.le_generateFrom_iff_subset_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α} : t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s | IsOpen s}
• isOpen_induced_eq 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α} : IsOpen s ↔ s ∈ Set.preimage f '' {s | IsOpen s}
• isOpen_sSup_iff 📋 Mathlib.Topology.Order
  {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)} : IsOpen s ↔ ∀ t ∈ T, IsOpen s
• generateFrom_iInter 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) : TopologicalSpace.generateFrom (⋂ i, {s | IsOpen s}) = ⨆ i, f i
• generateFrom_iUnion_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) : TopologicalSpace.generateFrom (⋃ i, {s | IsOpen s}) = ⨅ i, f i
• le_induced_generateFrom 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β} (h : ∀ a ∈ b, IsOpen (f ⁻¹' a)) : t ≤ TopologicalSpace.induced f (TopologicalSpace.generateFrom b)
• setOfPred_isOpen_iSup 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} : {s | IsOpen s} = ⋂ i, {s | IsOpen s}
• setOf_isOpen_iSup 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} : {s | IsOpen s} = ⋂ i, {s | IsOpen s}
• generateFrom_inter 📋 Mathlib.Topology.Order
  {α : Type u} (a b : TopologicalSpace α) : TopologicalSpace.generateFrom ({s | IsOpen s} ∩ {s | IsOpen s}) = a ⊔ b
• generateFrom_union_isOpen 📋 Mathlib.Topology.Order
  {α : Type u} (a b : TopologicalSpace α) : TopologicalSpace.generateFrom ({s | IsOpen s} ∪ {s | IsOpen s}) = a ⊓ b
• generateFrom_iInter_of_generateFrom_eq_self 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort v} (f : ι → Set (Set α)) (hf : ∀ (i : ι), {s | IsOpen s} = f i) : TopologicalSpace.generateFrom (⋂ i, f i) = ⨆ i, TopologicalSpace.generateFrom (f i)
• setOfPred_isOpen_sup 📋 Mathlib.Topology.Order
  {α : Type u} (t₁ t₂ : TopologicalSpace α) : {s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
• setOf_isOpen_sup 📋 Mathlib.Topology.Order
  {α : Type u} (t₁ t₂ : TopologicalSpace α) : {s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
• le_nhdsAdjoint_iff 📋 Mathlib.Topology.Order
  {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α) : t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
• eq_bot_of_singletons_open 📋 Mathlib.Topology.Order
  {α : Type u_1} {t : TopologicalSpace α} (h : ∀ (x : α), IsOpen {x}) : t = ⊥
• TopologicalSpace.isOpen_top_iff 📋 Mathlib.Topology.Order
  {α : Type u_2} (U : Set α) : IsOpen U ↔ U = ∅ ∨ U = Set.univ
• setOfPred_isOpen_sSup 📋 Mathlib.Topology.Order
  {α : Type u} {T : Set (TopologicalSpace α)} : {s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
• setOf_isOpen_sSup 📋 Mathlib.Topology.Order
  {α : Type u} {T : Set (TopologicalSpace α)} : {s | IsOpen s} = ⋂ t ∈ T, {s | IsOpen s}
• TopologicalSpace.gc_generateFrom 📋 Mathlib.Topology.Order
  (α : Type u_1) : GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
• TopologicalSpace.gciGenerateFrom 📋 Mathlib.Topology.Order
  (α : Type u_1) : GaloisCoinsertion (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
• IsOpen.nhdsSet_eq 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} : IsOpen s → nhdsSet s = Filter.principal s
• nhdsSet_eq_principal_iff 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} : nhdsSet s = Filter.principal s ↔ IsOpen s
• IsOpen.mem_nhdsSet_self 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} (ho : IsOpen s) : s ∈ nhdsSet s
• hasBasis_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] (s : Set X) : (nhdsSet s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U
• IsOpen.mem_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s t : Set X} (hU : IsOpen s) : s ∈ nhdsSet t ↔ t ⊆ s
• mem_nhdsSet_iff_exists 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s t : Set X} : s ∈ nhdsSet t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
• eventually_nhdsSet_iff_exists 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x
• IsOpenMap.isOpen_range 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) : IsOpen (Set.range f)
• Topology.IsInducing.isOpenMap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hi : Topology.IsInducing f) (ho : IsOpen (Set.range f)) : IsOpenMap f
• isClosedMap_iff_kernImage 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap f ↔ ∀ {u : Set X}, IsOpen u → IsOpen (Set.kernImage f u)
• Topology.IsCoinducing.isOpen_preimage 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsCoinducing f) {s : Set Y} : IsOpen (f ⁻¹' s) ↔ IsOpen s
• Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : (∀ (s : Set Y), IsOpen (f ⁻¹' s) ↔ IsOpen s) → Topology.IsCoinducing f
• Topology.IsOpenEmbedding.isOpen_iff_image_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s)
• Topology.isCoinducing_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsCoinducing f ↔ ∀ (s : Set Y), IsOpen (f ⁻¹' s) ↔ IsOpen s
• Topology.IsOpenEmbedding.isOpen_iff_preimage_isOpen 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {s : Set Y} (hs : s ⊆ Set.range f) : IsOpen s ↔ IsOpen (f ⁻¹' s)
• Topology.IsInducing.isOpen_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) {s : Set X} : IsOpen s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s
• Topology.IsInducing.setOfPred_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}
• 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}
• Topology.IsInducing.image_eq_isOpen_inter_range 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) {s : Set X} (hs : IsOpen s) : ∃ c, IsOpen c ∧ f '' s = c ∩ Set.range f
• Equiv.toHomeomorph 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : X ≃ₜ Y
• Equiv.toHomeomorph_refl 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} [TopologicalSpace X] : (Equiv.refl X).toHomeomorph ⋯ = Homeomorph.refl X
• Homeomorph.isOpen_image 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set X} : IsOpen (⇑h '' s) ↔ IsOpen s
• Homeomorph.isOpen_preimage 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y} : IsOpen (⇑h ⁻¹' s) ↔ IsOpen s
• Equiv.toEquiv_toHomeomorph 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).toEquiv = e
• Equiv.symm_toHomeomorph 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯
• Equiv.coe_toHomeomorph 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) : ⇑(e.toHomeomorph he) = ⇑e
• Equiv.toHomeomorph_apply 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (x : X) : (e.toHomeomorph he) x = e x
• Equiv.toHomeomorph_trans 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ Y) (f : Y ≃ Z) (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) (hf : ∀ (s : Set Z), IsOpen (⇑f ⁻¹' s) ↔ IsOpen s) : (e.trans f).toHomeomorph ⋯ = (e.toHomeomorph he).trans (f.toHomeomorph hf)
• 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
• SeparatedNhds.isOpen_union_iff 📋 Mathlib.Topology.Separation.SeparatedNhds
  {X : Type u_1} [TopologicalSpace X] {s t : Set X} (hst : SeparatedNhds s t) : IsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t
• isOpen_range_inl 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpen (Set.range Sum.inl)
• isOpen_range_inr 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpen (Set.range Sum.inr)
• IsOpen.prod 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ×ˢ t)
• isOpen_sum_iff 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X ⊕ Y)} : IsOpen s ↔ IsOpen (Sum.inl ⁻¹' s) ∧ IsOpen (Sum.inr ⁻¹' s)
• isOpen_setOfPred_disjoint_nhds_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} [TopologicalSpace X] : IsOpen {p | Disjoint (nhds p.1) (nhds p.2)}
• isOpen_setOf_disjoint_nhds_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} [TopologicalSpace X] : IsOpen {p | Disjoint (nhds p.1) (nhds p.2)}
• isOpen_prod_iff' 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} : IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
• prod_eq_generateFrom 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : instTopologicalSpaceProd = TopologicalSpace.generateFrom {g | ∃ s t, IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t}
• exists_nhds_square 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} [TopologicalSpace X] {s : Set (X × X)} {x : X} (hx : s ∈ nhds (x, x)) : ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s
• isOpen_prod_iff 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X × Y)} : IsOpen s ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
• mem_nhds_prod_iff' 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)} : s ∈ nhds (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s
• WithTopology.isOpen_iff 📋 Mathlib.Topology.WithTopology
  {X : Type u_1} (t : TopologicalSpace X) {s : Set (WithTopology X t)} : IsOpen s ↔ IsOpen (WithTopology.toTopology t ⁻¹' s)
• ULift.isOpen_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set (ULift.{v, u} X)} : IsOpen s ↔ IsOpen (ULift.up ⁻¹' s)
• isOpen_range_sigmaMk 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsOpen (Set.range (Sigma.mk i))
• CofiniteTopology.isOpen_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} {s : Set (CofiniteTopology X)} : IsOpen s ↔ s.Nonempty → sᶜ.Finite
• isOpen_sigma_fst_preimage 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] (s : Set ι) : IsOpen (Sigma.fst ⁻¹' s)
• CofiniteTopology.isOpen_iff' 📋 Mathlib.Topology.Constructions
  {X : Type u} {s : Set (CofiniteTopology X)} : IsOpen s ↔ s = ∅ ∨ sᶜ.Finite
• isOpen_sigma_iff 📋 Mathlib.Topology.Constructions
  {ι : Type u_2} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] {s : Set (Sigma σ)} : IsOpen s ↔ ∀ (i : ι), IsOpen (Sigma.mk i ⁻¹' s)
• frontier_inter_open_inter 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t
• IsOpen.preimage_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : IsOpen (Subtype.val ⁻¹' t)
• IsOpenMap.domRestrict 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenMap f) {s : Set X} (hs : IsOpen s) : IsOpenMap (s.domRestrict f)
• IsOpenMap.restrict 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenMap f) {s : Set X} (hs : IsOpen s) : IsOpenMap (s.domRestrict f)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59