Loogle!

Result

Found 16 declarations mentioning IsOpen and Set.Countable.

• TopologicalSpace.isOpen_sUnion_countable 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] (S : Set (Set α)) (H : ∀ s ∈ S, IsOpen s) : ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S
• TopologicalSpace.isOpen_iUnion_countable 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (s : ι → Set α) (H : ∀ (i : ι), IsOpen (s i)) : ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
• 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
• TopologicalSpace.isOpen_biUnion_countable 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (I : Set ι) (s : ι → Set α) (H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i
• eq_open_union_countable 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X) (h : ∀ (i : ι), IsOpen (U i)) : ∃ t, t.Countable ∧ ⋃ i ∈ t, U i = ⋃ i, U i
• isLindelof_of_countable_subcover 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) : IsLindelof s
• isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsLindelof (b i)) (U : Set X) : IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
• IsLindelof.elim_countable_subcover 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
• isLindelof_iff_countable_subcover 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsLindelof s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
• IsLindelof.elim_countable_subcover_image 📋 Mathlib.Topology.Compactness.Lindelof
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X} (hs : IsLindelof s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c 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)
• mem_residual_iff 📋 Mathlib.Topology.GDelta.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : s ∈ residual X ↔ ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s
• MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_3} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X} [SecondCountableTopology X] (hf : MeasureTheory.LocallyIntegrableOn f s μ) : ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, MeasureTheory.IntegrableOn f (u ∩ 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)
• ContinuousMap.secondCountableTopology 📋 Mathlib.Topology.ContinuousMap.SecondCountableSpace
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] (hX : ∃ S, S.Countable ∧ (∀ K ∈ S, IsCompact K) ∧ ∀ (f : C(X, Y)) (V : Set Y), IsOpen V → ∀ x ∈ ⇑f ⁻¹' V, ∃ K ∈ S, K ∈ nhds x ∧ Set.MapsTo (⇑f) K V) : SecondCountableTopology C(X, Y)

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 19971e9 serving mathlib revision 1bd7adb