Loogle!

Result

Found 2988 declarations whose name contains "basis". Of these, 91 have a name containing "exists" and "basis".

• Filter.HasBasis.exists_iff 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {P : Set α → Prop} (mono : ∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s) : (∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i)
• Disjoint.exists_mem_filter_basis 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (h : Disjoint l l') (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
• Module.Free.exists_basis 📋 Mathlib.LinearAlgebra.FreeModule.Basic
  (R : Type u) (M : Type v) {inst✝ : Semiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.Free R M] : Nonempty ((I : Type v) × Module.Basis I R M)
• finrank_eq_zero_of_not_exists_basis 📋 Mathlib.LinearAlgebra.Dimension.Finite
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] (h : ¬∃ s, Nonempty (Module.Basis (↑↑s) R M)) : Module.finrank R M = 0
• finrank_eq_zero_of_not_exists_basis_finite 📋 Mathlib.LinearAlgebra.Dimension.Finite
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] (h : ¬∃ s x, s.Finite) : Module.finrank R M = 0
• finrank_eq_zero_of_not_exists_basis_finset 📋 Mathlib.LinearAlgebra.Dimension.Finite
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] (h : ¬∃ s, Nonempty (Module.Basis (↥s) R M)) : Module.finrank R M = 0
• Module.Basis.exists_basis 📋 Mathlib.LinearAlgebra.Basis.VectorSpace
  (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : ∃ s, Nonempty (Module.Basis (↑s) K V)
• Set.PairwiseDisjoint.exists_mem_filter_basis 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} {I : Type u_6} {l : I → Filter α} {ι : I → Sort u_7} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} {S : Set I} (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) : ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
• Pairwise.exists_mem_filter_basis_of_disjoint 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} (hd : Pairwise (Function.onFun Disjoint l)) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) : ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Function.onFun Disjoint fun i => s i (ind i))
• Filter.exists_antitone_basis 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated] : ∃ x, f.HasAntitoneBasis x
• Filter.isCountablyGenerated_iff_exists_antitone_basis 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} {f : Filter α} : f.IsCountablyGenerated ↔ ∃ x, f.HasAntitoneBasis x
• Filter.HasBasis.exists_antitone_subbasis 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} {ι' : Sort u_5} {f : Filter α} [h : f.IsCountablyGenerated] {p : ι' → Prop} {s : ι' → Set α} (hs : f.HasBasis p s) : ∃ x, (∀ (i : ℕ), p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)
• Filter.Eventually.exists_mem_basis_of_smallSets 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ᶠ (t : Set α) in l.smallSets, P t) (h₂ : l.HasBasis p s) : ∃ i, p i ∧ P (s i)
• TopologicalSpace.exists_countable_basis 📋 Mathlib.Topology.Bases
  (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
• TopologicalSpace.IsTopologicalBasis.exists_countable 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : TopologicalSpace.IsTopologicalBasis t✝) : ∃ s ⊆ t✝, s.Countable ∧ TopologicalSpace.IsTopologicalBasis s
• TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis B) {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, v.Nonempty ∧ v ⊆ u
• TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u
• 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
• TopologicalSpace.IsTopologicalBasis.exists_subset_inter 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (self : TopologicalSpace.IsTopologicalBasis s) (t₁ : Set α) : t₁ ∈ s → ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
• LocallyFinite.exists_mem_basis 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ι → Set X} {ι' : Sort u_6} (hf : LocallyFinite f) {p : ι' → Prop} {s : ι' → Set X} {x : X} (hb : (nhds x).HasBasis p s) : ∃ i, p i ∧ {j | (f j ∩ s i).Nonempty}.Finite
• TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x y : X} (h : x ≠ y) : ∃ a ∈ b, x ∈ a ∧ y ∉ a
• Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : ι → Prop} {t : ι → Set X} {s : Set X} (hs : IsDiscrete s) {x : X} (hb : (nhds x).HasBasis p t) (hx : x ∈ s) : ∃ i, p i ∧ t i ∩ s = {x}
• TopologicalSpace.IsTopologicalBasis.exists_closure_subset 📋 Mathlib.Topology.Separation.Regular
  {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ nhds x) : ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s
• IsTopologicalAddGroup.exists_antitone_basis_nhds_zero 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type w) [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [FirstCountableTopology G] : ∃ u, (nhds 0).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) + u (n + 1) ⊆ u n
• IsTopologicalGroup.exists_antitone_basis_nhds_one 📋 Mathlib.Topology.Algebra.Group.Basic
  (G : Type w) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] [FirstCountableTopology G] : ∃ u, (nhds 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
• Filter.exists_forall_mem_of_hasBasis_mem_blimsup' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β} (hl : l.HasBasis (fun x => True) b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ Filter.blimsup u l p) : ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
• Filter.exists_forall_mem_of_hasBasis_mem_blimsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β} {q : ι → Prop} (hl : l.HasBasis q b) {u : β → Set α} {p : β → Prop} {x : α} (hx : x ∈ Filter.blimsup u l p) : ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
• PredOrder.hasBasis_nhds_Ioc_of_exists_gt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [PredOrder α] {a : α} (ha : ∃ u, a < u) : (nhds a).HasBasis (fun x => a < x) fun x => Set.Ico a x
• SuccOrder.hasBasis_nhds_Ioc_of_exists_lt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [SuccOrder α] {a : α} (ha : ∃ l, l < a) : (nhds a).HasBasis (fun x => x < a) fun x => Set.Ioc x a
• nhdsGE_basis_of_exists_gt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ u, a < u) : (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u
• nhdsLE_basis_of_exists_lt 📋 Mathlib.Topology.Order.Basic
  {α : Type u} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (ha : ∃ l, l < a) : (nhdsWithin a (Set.Iic a)).HasBasis (fun l => l < a) fun l => Set.Ioc l a
• nhdsGT_basis_of_exists_gt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ b, a < b) : (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioo a)
• nhdsLT_basis_of_exists_lt 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} (h : ∃ b, b < a) : (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ioo x a
• Disjoint.exists_uniform_thickening_of_basis 📋 Mathlib.Topology.UniformSpace.Compact
  {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)} (hU : (uniformity α).HasBasis p s) {A B : Set α} (hA : IsCompact A) (hB : IsClosed B) (h : Disjoint A B) : ∃ i, p i ∧ Disjoint (⋃ x ∈ A, UniformSpace.ball x (s i)) (⋃ x ∈ B, UniformSpace.ball x (s i))
• TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] {B : Set (TopologicalSpace.Opens α)} (hB : TopologicalSpace.Opens.IsBasis B) {U : TopologicalSpace.Opens α} (hU : IsCompact U.carrier) : ∃ Us ⊆ B, Us.Finite ∧ U = sSup Us
• LinearMap.BilinForm.exists_orthogonal_basis 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
  {V : Type u} {K : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [hK : Invertible 2] {B : LinearMap.BilinForm K V} (hB₂ : LinearMap.IsSymm B) : ∃ v, LinearMap.IsOrthoᵢ B ⇑v
• PowerBasis.exists_smodEq 📋 Mathlib.RingTheory.PowerBasis
  {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (pb : PowerBasis A B) (b : B) : ∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
• PowerBasis.exists_gen_dvd_sub 📋 Mathlib.RingTheory.PowerBasis
  {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [Algebra A B] (pb : PowerBasis A B) (b : B) : ∃ a, pb.gen ∣ b - (algebraMap A B) a
• PowerBasis.exists_eq_aeval' 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (pb : PowerBasis R S) (y : S) : ∃ f, y = (Polynomial.aeval pb.gen) f
• PowerBasis.exists_eq_aeval 📋 Mathlib.RingTheory.PowerBasis
  {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S] (pb : PowerBasis R S) (y : S) : ∃ f, f.natDegree < pb.dim ∧ y = (Polynomial.aeval pb.gen) f
• Algebra.norm_eq_one_of_not_exists_basis 📋 Mathlib.RingTheory.Norm.Defs
  (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (h : ¬∃ s, Nonempty (Module.Basis (↥s) R S)) (x : S) : (Algebra.norm R) x = 1
• LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap 📋 Mathlib.LinearAlgebra.PerfectPairing.Restrict
  {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup M] [AddCommGroup N] [Module L M] [Module L N] [Module K M] [Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] (M' : Submodule K M) (N' : Submodule K N) (hM : Submodule.span L ↑M' = ⊤) (hN : Submodule.span L ↑N' = ⊤) (hp : ∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range) : ∃ n b b', ∀ (i : Fin n), b i = ↑(b' i)
• MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis 📋 Mathlib.MeasureTheory.Measure.Typeclasses.Finite
  {α : Type u_1} {ι : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α} (hμ : μ.FiniteAtFilter f) {p : ι → Prop} {s : ι → Set α} (hf : f.HasBasis p s) : ∃ i, p i ∧ μ (s i) < ⊤
• Asymptotics.IsBigO.exists_mem_basis 📋 Mathlib.Analysis.Asymptotics.Defs
  {α : Type u_1} {E : Type u_3} {F' : Type u_7} [Norm E] [SeminormedAddCommGroup F'] {f : α → E} {g' : α → F'} {l : Filter α} {ι : Sort u_18} {p : ι → Prop} {s : ι → Set α} (h : f =O[l] g') (hb : l.HasBasis p s) : ∃ c > 0, ∃ i, p i ∧ ∀ x ∈ s i, ‖f x‖ ≤ c * ‖g' x‖
• AffineBasis.exists_affineBasis 📋 Mathlib.LinearAlgebra.AffineSpace.Basis
  (k : Type u_5) (V : Type u_6) (P : Type u_7) [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] : ∃ s b, ⇑b = Subtype.val
• AffineBasis.exists_affine_subbasis 📋 Mathlib.LinearAlgebra.AffineSpace.Basis
  {k : Type u_5} {V : Type u_6} {P : Type u_7} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] {t : Set P} (ht : affineSpan k t = ⊤) : ∃ s ⊆ t, ∃ b, ⇑b = Subtype.val
• Module.Basis.exists_opNorm_le 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Module.Basis ι 𝕜 E) : ∃ C > 0, ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ (i : ι), ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M
• Module.Basis.exists_opNNNorm_le 📋 Mathlib.Analysis.Normed.Module.FiniteDimension
  {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace 𝕜] {ι : Type u_1} [Finite ι] (v : Module.Basis ι 𝕜 E) : ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : NNReal), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
• Orthonormal.exists_orthonormalBasis_extension_of_card_eq 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_7} [Fintype ι] (card_ι : Module.finrank 𝕜 E = Fintype.card ι) {v : ι → E} {s : Set ι} (hv : Orthonormal 𝕜 (s.restrict v)) : ∃ b, ∀ i ∈ s, b i = v i
• exists_orthonormalBasis 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : ∃ w b, ⇑b = Subtype.val
• Orthonormal.exists_orthonormalBasis_extension 📋 Mathlib.Analysis.InnerProductSpace.PiL2
  {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) : ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val
• WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
  {R : Type r} [CommRing R] {W' : WeierstrassCurve.Affine R} (x : W'.CoordinateRing) : ∃ p q, p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X = x
• Matroid.exists_isBasis' 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} (M : Matroid α) (X : Set α) : ∃ I, M.IsBasis' I X
• Matroid.exists_isBasis 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : ∃ I, M.IsBasis I X
• Matroid.IsBasis.exists_isBase 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) : ∃ B, M.IsBase B ∧ I = B ∩ X
• Matroid.exists_isBasis_subset_isBasis 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ I J, M.IsBasis I X ∧ M.IsBasis J Y ∧ I ⊆ J
• Matroid.IsBasis.exists_isBasis_inter_eq_of_superset 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.IsBasis I X) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ J, M.IsBasis J Y ∧ J ∩ X = I
• Matroid.exists_isBasis_union_inter_isBasis 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} (M : Matroid α) (X Y : Set α) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : ∃ I, M.IsBasis I (X ∪ Y) ∧ M.IsBasis (I ∩ Y) Y
• Matroid.exists_isBasis_disjoint_isBasis_of_subset 📋 Mathlib.Combinatorics.Matroid.Basic
  {α : Type u_1} (M : Matroid α) {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ I J, M.IsBasis I X ∧ M.IsBasis (I ∪ J) Y ∧ Disjoint X J
• Matroid.Indep.exists_isBasis_subset_union_isBasis 📋 Mathlib.Combinatorics.Matroid.Minor.Restrict
  {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hJ : M.IsBasis J X) : ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
• Matroid.Indep.exists_insert_of_not_isBasis 📋 Mathlib.Combinatorics.Matroid.Minor.Restrict
  {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hI' : ¬M.IsBasis I X) (hJ : M.IsBasis J X) : ∃ e ∈ J \ I, M.Indep (insert e I)
• Matroid.exists_isBasis_inter_ground_isBasis_closure 📋 Mathlib.Combinatorics.Matroid.Closure
  {α : Type u_2} (M : Matroid α) (X : Set α) : ∃ I, M.IsBasis I (X ∩ M.E) ∧ M.IsBasis I (M.closure X)
• Matroid.IsRkFinite.exists_finite_isBasis' 📋 Mathlib.Combinatorics.Matroid.Rank.Finite
  {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : ∃ I, M.IsBasis' I X ∧ I.Finite
• Matroid.isRkFinite_iff_exists_isBasis' 📋 Mathlib.Combinatorics.Matroid.Rank.Finite
  {α : Type u_1} {M : Matroid α} {X : Set α} : M.IsRkFinite X ↔ ∃ I, M.IsBasis' I X ∧ I.Finite
• Matroid.IsRkFinite.exists_finset_isBasis' 📋 Mathlib.Combinatorics.Matroid.Rank.Finite
  {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.IsRkFinite X) : ∃ I, M.IsBasis' (↑I) X
• exists_isTranscendenceBasis' 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  (R : Type u_1) (A : Type w) [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] : ∃ ι x, IsTranscendenceBasis R x
• exists_isTranscendenceBasis 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  (R : Type u_1) (A : Type w) [CommRing R] [CommRing A] [Algebra R A] [FaithfulSMul R A] : ∃ s, IsTranscendenceBasis R Subtype.val
• exists_isTranscendenceBasis_superset 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  {R : Type u_1} {A : Type w} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} (hs : AlgebraicIndepOn R id s) : ∃ t, s ⊆ t ∧ IsTranscendenceBasis R Subtype.val
• isAlgebraic_iff_exists_isTranscendenceBasis_subset 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  {R : Type u_1} {A : Type w} [CommRing R] [CommRing A] [Algebra R A] [IsDomain A] [FaithfulSMul R A] {s : Set A} : Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A ↔ ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
• exists_isTranscendenceBasis_subset 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  {R : Type u_1} {A : Type w} [CommRing R] [CommRing A] [Algebra R A] [NoZeroDivisors A] [FaithfulSMul R A] (s : Set A) [Algebra.IsAlgebraic (↥(Algebra.adjoin R s)) A] : ∃ t ⊆ s, IsTranscendenceBasis R Subtype.val
• exists_isTranscendenceBasis_between 📋 Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
  {R : Type u_1} {A : Type w} [CommRing R] [CommRing A] [Algebra R A] [NoZeroDivisors A] (s t : Set A) (hst : s ⊆ t) (hs : AlgebraicIndepOn R id s) [ht : Algebra.IsAlgebraic (↥(Algebra.adjoin R t)) A] : ∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R Subtype.val
• IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure 📋 Mathlib.FieldTheory.SeparableClosure
  (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (Hfg : ⊤.FG) : ∃ s, MaximalFor (fun t => IsTranscendenceBasis F Subtype.val) (fun t => IntermediateField.restrictScalars F (separableClosure (↥(IntermediateField.adjoin F t)) E)) ↑s
• Algebra.trace_eq_zero_of_not_exists_basis 📋 Mathlib.RingTheory.Trace.Defs
  (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (h : ¬∃ s, Nonempty (Module.Basis (↥s) R S)) : Algebra.trace R S = 0
• FiniteDimensional.exists_is_basis_integral 📋 Mathlib.RingTheory.DedekindDomain.IntegralClosure
  (A : Type u_1) (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [FiniteDimensional K L] [IsDomain A] : ∃ s b, ∀ (x : ↥s), IsIntegral A (b x)
• AffineBasis.exists_affineBasis_of_finiteDimensional 📋 Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
  {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [AddCommGroup V] [AddTorsor V P] [DivisionRing k] [Module k V] [Fintype ι] [FiniteDimensional k V] (h : Fintype.card ι = Module.finrank k V + 1) : Nonempty (AffineBasis ι k P)
• exists_mem_interior_convexHull_affineBasis 📋 Mathlib.Analysis.Normed.Affine.Convex
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E} (hs : s ∈ nhds x) : ∃ b, x ∈ interior ((convexHull ℝ) (Set.range ⇑b)) ∧ (convexHull ℝ) (Set.range ⇑b) ⊆ s
• exists_hilbertBasis 📋 Mathlib.Analysis.InnerProductSpace.l2Space
  (𝕜 : Type u_2) [RCLike 𝕜] (E : Type u_3) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : ∃ w b, ⇑b = Subtype.val
• Orthonormal.exists_hilbertBasis_extension 📋 Mathlib.Analysis.InnerProductSpace.l2Space
  {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {s : Set E} (hs : Orthonormal 𝕜 Subtype.val) : ∃ w b, s ⊆ w ∧ ⇑b = Subtype.val
• exists_isTranscendenceBasis_and_isSeparable_of_perfectField 📋 Mathlib.FieldTheory.SeparablyGenerated
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [PerfectField k] (Hfg : ⊤.FG) : ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K
• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow 📋 Mathlib.FieldTheory.SeparablyGenerated
  {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) {a : ι → K} (n : ι) [ExpChar k p] (ha' : IsTranscendenceBasis k fun i => a ↑i) : ∃ i, (IsTranscendenceBasis k fun j => a ↑j) ∧ IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) (a i)
• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_fg 📋 Mathlib.FieldTheory.SeparablyGenerated
  {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) [ExpChar k p] (Hfg : ⊤.FG) : ∃ s, IsTranscendenceBasis k Subtype.val ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k ↑s)) K
• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow' 📋 Mathlib.FieldTheory.SeparablyGenerated
  {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) {a : ι → K} [ExpChar k p] (s : Set ι) (n : ι) (ha : IsTranscendenceBasis k fun i => a ↑i) (hn : n ∉ s) : ∃ i, (IsTranscendenceBasis k fun j => a ↑j) ∧ IsSeparable (↥(IntermediateField.adjoin k (a '' (insert n s \ {i})))) (a i)
• exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top 📋 Mathlib.FieldTheory.SeparablyGenerated
  {k : Type u_1} {K : Type u_2} {ι : Type u_3} [Field k] [Field K] [Algebra k K] (p : ℕ) (hp : Nat.Prime p) (H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) {a : ι → K} (n : ι) [ExpChar k p] (ha : IntermediateField.adjoin k (Set.range a) = ⊤) (ha' : IsTranscendenceBasis k fun i => a ↑i) : ∃ i, (IsTranscendenceBasis k fun j => a ↑j) ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) K
• Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq 📋 Mathlib.GroupTheory.Perm.Centralizer
  {α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} (a : g.Basis) (x : α) : x ∈ Function.fixedPoints ⇑g ∨ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
• Module.exists_basis_of_span_of_flat 📋 Mathlib.RingTheory.LocalRing.Module
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] [Module.Flat R M] {ι : Type u} (v : ι → M) (hv : Submodule.span R (Set.range v) = ⊤) : ∃ κ a b, ∀ (i : κ), b i = v (a i)
• Module.exists_basis_of_span_of_maximalIdeal_rTensor_injective 📋 Mathlib.RingTheory.LocalRing.Module
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] (H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R)))) {ι : Type u} (v : ι → M) (hv : Submodule.span R (Set.range v) = ⊤) : ∃ κ a b, ∀ (i : κ), b i = v (a i)
• Module.exists_basis_of_basis_baseChange 📋 Mathlib.RingTheory.LocalRing.Module
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsLocalRing R] [Module.FinitePresentation R M] {ι : Type u_5} (v : ι → M) (hli : LinearIndependent (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v)) (hsp : Submodule.span (IsLocalRing.ResidueField R) (Set.range (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v)) = ⊤) (H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (IsLocalRing.maximalIdeal R)))) : ∃ b, ∀ (i : ι), b i = v i
• Module.FinitePresentation.exists_basis_localizedModule_powers 📋 Mathlib.RingTheory.Localization.Free
  {R : Type u_4} {M : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (Rₛ : Type u_3) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M'] [IsLocalization S Rₛ] [Module.FinitePresentation R M] {I : Type u_6} [Finite I] (b : Module.Basis I Rₛ M') : ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i
• Algebra.Generators.exists_presentation_of_basis_cotangent 📋 Mathlib.RingTheory.Extension.Cotangent.Basis
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] {α : Type u_4} (P : Algebra.Generators R S α) [Finite α] {σ : Type u_5} (b₀ : Module.Basis σ S P.toExtension.Cotangent) : ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Algebra.Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
• Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential 📋 Mathlib.RingTheory.Smooth.StandardSmoothOfFree
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S] : Algebra.IsStandardSmooth R S ↔ Subsingleton (Algebra.H1Cotangent R S) ∧ ∃ I b, Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)
• IsCompactOpenCovered.exists_mem_of_isBasis 📋 Mathlib.Topology.Sets.CompactOpenCovered
  {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [(i : ι) → TopologicalSpace (X i)] {B : (i : ι) → Set (TopologicalSpace.Opens (X i))} (hB : ∀ (i : ι), TopologicalSpace.Opens.IsBasis (B i)) (hBc : ∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier) {U : Set S} (hU : IsCompactOpenCovered f U) : ∃ n a V, (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' ↑(V i) = 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 6ec3a4c