Loogle!
Result
Found 1444 declarations mentioning Set.Finite. Of these, only the first 200 are shown.
- Set.Finite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} (s : Set α) : Prop - Set.finite_or_infinite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} (s : Set α) : s.Finite ∨ s.Infinite - Set.infinite_or_finite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} (s : Set α) : s.Infinite ∨ s.Finite - Set.toFinite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} (s : Set α) [Finite ↑s] : s.Finite - Set.Finite.not_infinite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} : s.Finite → ¬s.Infinite - Set.Finite.to_subtype 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} (h : s.Finite) : Finite ↑s - Set.Infinite.not_finite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} (hs : s.Infinite) : ¬s.Finite - Set.finite_coe_iff 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} : Finite ↑s ↔ s.Finite - Set.not_finite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} : ¬s.Finite ↔ s.Infinite - Set.not_infinite 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {s : Set α} : ¬s.Infinite ↔ s.Finite - Equiv.set_finite_iff 📋 Mathlib.Basic.Finite.Defs
{α : Type u} {β : Type v} {s : Set α} {t : Set β} (hst : ↑s ≃ ↑t) : s.Finite ↔ t.Finite - Finite.of_finite_univ 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : Set.univ.Finite → Finite α - Set.finite_univ 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Finite α] : Set.univ.Finite - Set.fintypeOfFiniteUniv 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (H : Set.univ.Finite) : Fintype α - Set.finite_empty 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : ∅.Finite - Set.finite_univ_iff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : Set.univ.Finite ↔ Finite α - Set.Finite.of_subsingleton 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Subsingleton α] (s : Set α) : s.Finite - Set.Finite.toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) : Finset α - Set.univ_finite_iff_nonempty_fintype 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : Set.univ.Finite ↔ Nonempty (Fintype α) - Set.Subsingleton.finite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Subsingleton) : s.Finite - Set.finite_range_const 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {c : β} : (Set.range fun x => c).Finite - Set.Finite.fintype 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) : Fintype ↑s - Set.Finite.inhabited 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : Inhabited { s // s.Finite } - Set.finite_le_nat 📋 Mathlib.Data.Set.Finite.Basic
(n : ℕ) : {i | i ≤ n}.Finite - Set.finite_lt_nat 📋 Mathlib.Data.Set.Finite.Basic
(n : ℕ) : {i | i < n}.Finite - Set.finite_singleton 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (a : α) : {a}.Finite - Set.Finite.nonempty_fintype 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} : s.Finite → Nonempty (Fintype ↑s) - Finset.finite_toSet 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (s : Finset α) : (↑s).Finite - Set.finite_def 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} : s.Finite ↔ Nonempty (Fintype ↑s) - Set.instCanLiftFinsetCoeFinite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : CanLift (Set α) (Finset α) SetLike.coe Set.Finite - List.finite_toSet 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (l : List α) : {x | x ∈ l}.Finite - Multiset.finite_toSet 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (s : Multiset α) : {x | x ∈ s}.Finite - Set.infinite_of_finite_compl 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Infinite α] {s : Set α} (hs : sᶜ.Finite) : s.Infinite - Set.Finite.finite_of_compl 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (hsc : sᶜ.Finite) : Finite α - Set.Finite.image 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} (f : α → β) (hs : s.Finite) : (f '' s).Finite - Set.Finite.infinite_compl 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Infinite α] {s : Set α} (hs : s.Finite) : sᶜ.Infinite - Set.Finite.toFinset_nonempty 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) : hs.toFinset.Nonempty ↔ s.Nonempty - Set.Finite.toFinset_nontrivial 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) : h.toFinset.Nontrivial ↔ s.Nontrivial - Set.finite_range_iff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} (hf : Function.Injective f) : (Set.range f).Finite ↔ Finite α - Set.Finite.diff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Finite) : (s \ t).Finite - Set.Finite.insert 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (a : α) {s : Set α} (hs : s.Finite) : (insert a s).Finite - Set.Finite.inter_of_left 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (t : Set α) : (s ∩ t).Finite - Set.Finite.inter_of_right 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (t : Set α) : (t ∩ s).Finite - Set.Finite.sdiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Finite) : (s \ t).Finite - Set.finite_insert 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {a : α} : (insert a s).Finite ↔ s.Finite - Set.Finite.map 📋 Mathlib.Data.Set.Finite.Basic
{α β : Type u_1} {s : Set α} (f : α → β) : s.Finite → (f <$> s).Finite - Set.Finite.subset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) {t : Set α} (ht : t ⊆ s) : t.Finite - Set.Finite.toFinset_univ 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Fintype α] (h : Set.univ.Finite) : h.toFinset = Finset.univ - Finset.forall 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {p : Finset α → Prop} : (∀ (s : Finset α), p s) ↔ ∀ (s : Set α) (hs : s.Finite), p hs.toFinset - Set.finite_mem_finset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (s : Finset α) : {a | a ∈ s}.Finite - Set.Finite.coe_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) : ↑hs.toFinset = s - Set.Finite.exists_notMem 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} [Infinite α] (hs : s.Finite) : ∃ a, a ∉ s - Set.Finite.of_diff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite - Set.Finite.of_preimage 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : (f ⁻¹' s).Finite) (hf : Function.Surjective f) : s.Finite - Set.Finite.of_sdiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hd : (s \ t).Finite) (ht : t.Finite) : s.Finite - Set.Finite.of_surjOn 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} {t : Set β} (f : α → β) (hf : Set.SurjOn f s t) (hs : s.Finite) : t.Finite - Set.Finite.union 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Finite) (ht : t.Finite) : (s ∪ t).Finite - Set.Infinite.diff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : (s \ t).Infinite - Set.Infinite.sdiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : (s \ t).Infinite - Set.BijOn.finite_iff_finite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β} (h : Set.BijOn f s t) : s.Finite ↔ t.Finite - Set.Finite.of_finite_image 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} {f : α → β} (h : (f '' s).Finite) (hi : Set.InjOn f s) : s.Finite - Set.Finite.toFinset_eq_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} [Fintype ↑s] (h : s.Finite) : h.toFinset = s.toFinset - Set.finite_image_iff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} {f : α → β} (hi : Set.InjOn f s) : (f '' s).Finite ↔ s.Finite - Set.finite_range_findGreatest 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {P : α → ℕ → Prop} [(x : α) → DecidablePred (P x)] {b : ℕ} : (Set.range fun x => Nat.findGreatest (P x) b).Finite - Set.finite_union 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} : (s ∪ t).Finite ↔ s.Finite ∧ t.Finite - Set.not_injOn_infinite_finite_image 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set α} (h_inf : s.Infinite) (h_fin : (f '' s).Finite) : ¬Set.InjOn f s - Set.Finite.exists_finset_coe 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) : ∃ s', ↑s' = s - Set.Finite.card_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} [Fintype ↑s] (h : s.Finite) : h.toFinset.card = Fintype.card ↑s - Set.Finite.sep 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (p : α → Prop) : {a | a ∈ s ∧ p a}.Finite - Set.Finite.toFinset_empty 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (h : ∅.Finite) : h.toFinset = ∅ - Set.Finite.of_injOn 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β} (hm : Set.MapsTo f s t) (hi : Set.InjOn f s) (ht : t.Finite) : s.Finite - Set.Finite.preimage 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set β} (I : Set.InjOn f (f ⁻¹' s)) (h : s.Finite) : (f ⁻¹' s).Finite - Set.Finite.toFinset_eq_univ 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} [Fintype α] {h : s.Finite} : h.toFinset = Finset.univ ↔ s = Set.univ - Set.finite_of_finite_preimage 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : (f ⁻¹' s).Finite) (hs : s ⊆ Set.range f) : s.Finite - Set.Finite.injOn_iff_bijOn_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : Set.MapsTo f s s) : Set.InjOn f s ↔ Set.BijOn f s s - Set.Infinite.inter_of_finite_diff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u_1} {s t : Set α} (hs : s.Infinite) (ht : (s \ t).Finite) : (s ∩ t).Infinite - Set.Infinite.inter_of_finite_sdiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u_1} {s t : Set α} (hs : s.Infinite) (ht : (s \ t).Finite) : (s ∩ t).Infinite - Set.finite_option 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set (Option α)} : s.Finite ↔ {x | some x ∈ s}.Finite - Set.Finite.preimage_embedding 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set β} (f : α ↪ β) (h : s.Finite) : (⇑f ⁻¹' s).Finite - Set.Finite.surjOn_iff_bijOn_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {f : α → α} (hs : s.Finite) (hm : Set.MapsTo f s s) : Set.SurjOn f s s ↔ Set.BijOn f s s - Finset.mem_range_coe_iff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} : s ∈ Set.range SetLike.coe ↔ s.Finite - Set.Finite.toFinset_eq_empty 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {h : s.Finite} : h.toFinset = ∅ ↔ s = ∅ - Set.Finite.toFinset_inj 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : hs.toFinset = ht.toFinset ↔ s = t - Finset.exists 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {p : Finset α → Prop} : (∃ s, p s) ↔ ∃ s, ∃ (hs : s.Finite), p hs.toFinset - Set.exists_finite_iff_finset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {p : Set α → Prop} : (∃ s, s.Finite ∧ p s) ↔ ∃ s, p ↑s - Set.Finite.coeSort_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) : ↥hs.toFinset = ↑s - OrderIso.finsetSetFinite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : Finset α ≃o { s // s.Finite } - Set.Finite.ofFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {p : Set α} (s : Finset α) (H : ∀ (x : α), x ∈ s ↔ x ∈ p) : p.Finite - Set.Finite.mem_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {a : α} (hs : s.Finite) : a ∈ hs.toFinset ↔ a ∈ s - Set.Finite.toFinset_range 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} [DecidableEq α] [Fintype β] (f : β → α) (h : (Set.range f).Finite) : h.toFinset = Finset.image f Finset.univ - Set.Infinite.exists_notMem_finite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Infinite) (ht : t.Finite) : ∃ a ∈ s, a ∉ t - Set.seq_of_forall_finite_exists 📋 Mathlib.Data.Set.Finite.Basic
{γ : Type u_1} {P : γ → Set γ → Prop} (h : ∀ (t : Set γ), t.Finite → ∃ c, P c t) : ∃ u, ∀ (n : ℕ), P (u n) (u '' Set.Iio n) - Set.Finite.exists_finset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) : ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s - Set.finite_preimage_inl_and_inr 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set (α ⊕ β)} : (Sum.inl ⁻¹' s).Finite ∧ (Sum.inr ⁻¹' s).Finite ↔ s.Finite - Set.Finite.inf_of_left 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) (t : Set α) : (s ⊓ t).Finite - Set.Finite.inf_of_right 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (h : s.Finite) (t : Set α) : (t ⊓ s).Finite - Set.Finite.toFinset_ofPred 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Fintype α] (p : α → Prop) [DecidablePred p] (h : {x | p x}.Finite) : h.toFinset = {x | p x} - Set.Finite.toFinset_setOf 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [Fintype α] (p : α → Prop) [DecidablePred p] (h : {x | p x}.Finite) : h.toFinset = {x | p x} - Set.Finite.toFinset_singleton 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {a : α} (ha : {a}.Finite := ⋯) : ha.toFinset = {a} - Set.Finite.subtypeEquivToFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) : { x // x ∈ s } ≃ ↥hs.toFinset - Set.Finite.toFinset_mono 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : s ⊆ t → hs.toFinset ⊆ ht.toFinset - Set.Finite.subset_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} : s ⊆ ht.toFinset ↔ ↑s ⊆ t - Set.Finite.sup 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} : s.Finite → t.Finite → (s ⊔ t).Finite - Set.Finite.toFinset_image 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} [DecidableEq β] (f : α → β) (hs : s.Finite) (h : (f '' s).Finite) : h.toFinset = Finset.image f hs.toFinset - Set.Finite.toFinset_subset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} : hs.toFinset ⊆ t ↔ s ⊆ ↑t - Set.Finite.toFinset_subset_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t - Set.finite_range_ite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {p : α → Prop} [DecidablePred p] {f g : α → β} (hf : (Set.range f).Finite) (hg : (Set.range g).Finite) : (Set.range fun x => if p x then f x else g x).Finite - Set.Finite.toFinset_insert' 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [DecidableEq α] {a : α} {s : Set α} (hs : s.Finite) : ⋯.toFinset = insert a hs.toFinset - Set.Finite.symmDiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} (hs : s.Finite) (ht : t.Finite) : (symmDiff s t).Finite - instWellFoundedLTSubtypeSetFinite 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} : WellFoundedLT { s // s.Finite } - Set.Finite.toFinset_compl 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} [DecidableEq α] [Fintype α] (hs : s.Finite) (h : sᶜ.Finite) : h.toFinset = hs.toFinsetᶜ - Set.Finite.toFinset_inter 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∩ t).Finite) : h.toFinset = hs.toFinset ∩ ht.toFinset - Set.Finite.toFinset_sdiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s \ t).Finite) : h.toFinset = hs.toFinset \ ht.toFinset - Set.Finite.toFinset_union 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∪ t).Finite) : h.toFinset = hs.toFinset ∪ ht.toFinset - Set.Finite.induction_on 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (insert a s) ⋯) : motive s hs - Set.Infinite.exists_ne_map_eq_of_mapsTo 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : α → β} (hs : s.Infinite) (hf : Set.MapsTo f s t) (ht : t.Finite) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y - Set.exists_subset_image_finite_and 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {β : Type v} {f : α → β} {s : Set α} {p : Set β → Prop} : (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t) - Set.Finite.toFinset_insert 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [DecidableEq α] {s : Set α} {a : α} (hs : (insert a s).Finite) : hs.toFinset = insert a ⋯.toFinset - Set.Finite.toFinset_strictMono 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : s ⊂ t → hs.toFinset ⊂ ht.toFinset - Set.Finite.ssubset_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {t : Set α} {ht : t.Finite} {s : Finset α} : s ⊂ ht.toFinset ↔ ↑s ⊂ t - Set.Finite.toFinset_ssubset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} {hs : s.Finite} {t : Finset α} : hs.toFinset ⊂ t ↔ s ⊂ ↑t - Set.Finite.toFinset_ssubset_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t - Set.Finite.disjoint_toFinset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t - Set.finite_of_forall_not_lt_lt 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} [LinearOrder α] {s : Set α} (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) : s.Finite - Set.Finite.induction_on_subset 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {motive : (s : Set α) → s.Finite → Prop} (s : Set α) (hs : s.Finite) (empty : motive ∅ ⋯) (insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (insert a t) ⋯) : motive s hs - Set.Finite.symmDiff_congr 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t u : Set α} (hst : (symmDiff s t).Finite) : (symmDiff s u).Finite ↔ (symmDiff t u).Finite - Set.Finite.toFinset_symmDiff 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s t : Set α} [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (symmDiff s t).Finite) : h.toFinset = symmDiff hs.toFinset ht.toFinset - OrderIso.finsetSetFinite_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (s : Finset α) : ↑(OrderIso.finsetSetFinite s) = ↑s - Set.Finite.subtypeEquivToFinset_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (a : { a // a ∈ s }) : ↑(hs.subtypeEquivToFinset a) = ↑a - OrderIso.finsetSetFinite_symm_apply 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} (s : { s // s.Finite }) : (RelIso.symm OrderIso.finsetSetFinite) s = ⋯.toFinset - Set.Finite.subtypeEquivToFinset_symm_apply_coe 📋 Mathlib.Data.Set.Finite.Basic
{α : Type u} {s : Set α} (hs : s.Finite) (b : ↥hs.toFinset) : ↑(hs.subtypeEquivToFinset.symm b) = ↑b - Set.Finite.pi 📋 Mathlib.Data.Fintype.Pi
{ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) : (Set.univ.pi t).Finite - Set.forall_finite_image_eval_iff 📋 Mathlib.Data.Fintype.Pi
{δ : Type u_3} [Finite δ] {κ : δ → Type u_4} {s : Set ((d : δ) → κ d)} : (∀ (d : δ), (Function.eval d '' s).Finite) ↔ s.Finite - Set.Finite.pi' 📋 Mathlib.Data.Fintype.Pi
{ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)} (ht : ∀ (i : ι), (t i).Finite) : {f | ∀ (i : ι), f i ∈ t i}.Finite - Set.Finite.offDiag 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {s : Set α} (hs : s.Finite) : s.offDiag.Finite - Set.Finite.image2 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) : (Set.image2 f s t).Finite - Set.Finite.toFinset_offDiag 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {s : Set α} (hs : s.Finite) : ⋯.toFinset = hs.toFinset.offDiag - Set.Finite.of_prod_left 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) : t.Nonempty → s.Finite - Set.Finite.of_prod_right 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (h : (s ×ˢ t).Finite) : s.Nonempty → t.Finite - Set.Finite.prod 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) : (s ×ˢ t).Finite - Set.finite_image_fst_and_snd_iff 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set (α × β)} : (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite - Set.finite_prod 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) - Set.Finite.toFinset_prod 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) : hs.toFinset ×ˢ ht.toFinset = ⋯.toFinset - Set.finite_image2 📋 Mathlib.Basic.Finite.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (hfs : ∀ b ∈ t, Set.InjOn (fun x => f x b) s) (hft : ∀ a ∈ s, Set.InjOn (f a) t) : (Set.image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ - Set.finite_one 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [One α] : Set.Finite 1 - Set.finite_zero 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Zero α] : Set.Finite 0 - Set.Finite.inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s.Finite → s⁻¹.Finite - Set.Finite.neg 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveNeg α] {s : Set α} : s.Finite → (-s).Finite - Set.Finite.of_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹.Finite → s.Finite - Set.Finite.of_neg 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveNeg α] {s : Set α} : (-s).Finite → s.Finite - Set.finite_inv 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveInv α] {s : Set α} : s⁻¹.Finite ↔ s.Finite - Set.finite_neg 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [InvolutiveNeg α] {s : Set α} : (-s).Finite ↔ s.Finite - Set.Finite.vsub 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} {β : Type u_2} [VSub α β] {s t : Set β} (hs : s.Finite) (ht : t.Finite) : (s -ᵥ t).Finite - Set.Finite.smul_set 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} {β : Type u_2} [SMul α β] {s : Set β} {a : α} : s.Finite → (a • s).Finite - Set.Finite.vadd_set 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} {β : Type u_2} [VAdd α β] {s : Set β} {a : α} : s.Finite → (a +ᵥ s).Finite - Set.Finite.add 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Add α] {s t : Set α} : s.Finite → t.Finite → (s + t).Finite - Set.Finite.div 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Div α] {s t : Set α} : s.Finite → t.Finite → (s / t).Finite - Set.Finite.mul 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Mul α] {s t : Set α} : s.Finite → t.Finite → (s * t).Finite - Set.Finite.sub 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Sub α] {s t : Set α} : s.Finite → t.Finite → (s - t).Finite - Set.Finite.smul 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} {β : Type u_2} [SMul α β] {s : Set α} {t : Set β} : s.Finite → t.Finite → (s • t).Finite - Set.Finite.vadd 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} {β : Type u_2} [VAdd α β] {s : Set α} {t : Set β} : s.Finite → t.Finite → (s +ᵥ t).Finite - Set.finite_div 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Group α] {s t : Set α} : (s / t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ - Set.finite_sub 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [AddGroup α] {s t : Set α} : (s - t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ - Set.finite_add 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s t : Set α} : (s + t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ - Set.finite_mul 📋 Mathlib.Algebra.Group.Pointwise.Set.Finite
{α : Type u_1} [Mul α] [IsLeftCancelMul α] [IsRightCancelMul α] {s t : Set α} : (s * t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ - Set.Finite.powerset 📋 Mathlib.Data.Set.Finite.Powerset
{α : Type u} {s : Set α} (h : s.Finite) : (𝒫 s).Finite - Set.Finite.finite_subsets 📋 Mathlib.Data.Set.Finite.Powerset
{α : Type u} {a : Set α} (h : a.Finite) : {b | b ⊆ a}.Finite - Set.finite_range 📋 Mathlib.Data.Set.Finite.Range
{α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] : (Set.range f).Finite - Set.Finite.dependent_image 📋 Mathlib.Data.Set.Finite.Range
{α : Type u} {β : Type v} {s : Set α} (hs : s.Finite) (F : (i : α) → i ∈ s → β) : {y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite - Set.Finite.exists_subset_finite_image_eq 📋 Mathlib.Data.Set.Finite.Range
{α : Type u} {β : Type v} {f : α → β} {s : Set α} {u : Set β} (hu : u.Finite) (hsu : u ⊆ f '' s) : ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u - Set.finite_iUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Sort w} [Finite ι] {f : ι → Set α} (H : ∀ (i : ι), (f i).Finite) : (⋃ i, f i).Finite - Set.finite_iUnion_of_subsingleton 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Sort u_1} [Subsingleton ι] {s : ι → Set α} : (⋃ i, s i).Finite ↔ ∀ (i : ι), (s i).Finite - Set.Finite.bddAbove 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [Preorder α] [IsDirectedOrder α] [Nonempty α] {s : Set α} (hs : s.Finite) : BddAbove s - Set.Finite.bddBelow 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [Preorder α] [IsCodirectedOrder α] [Nonempty α] {s : Set α} (hs : s.Finite) : BddBelow s - Set.Finite.sInter 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : t ∈ s) (hf : t.Finite) : (⋂₀ s).Finite - Set.union_finset_finite_of_range_finite 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} (f : α → Finset β) (h : (Set.range f).Finite) : (⋃ a, ↑(f a)).Finite - Set.Finite.sUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {s : Set (Set α)} (hs : s.Finite) (H : ∀ t ∈ s, t.Finite) : (⋃₀ s).Finite - Set.Finite.preimage' 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} {f : α → β} {s : Set β} (h : s.Finite) (hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite) : (f ⁻¹' s).Finite - Set.Finite.of_finite_fibers 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} (f : α → β) {s : Set α} (himage : (f '' s).Finite) (hfibers : ∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) : s.Finite - Set.Finite.biUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : ι → Set α} (ht : ∀ i ∈ s, (t i).Finite) : (⋃ i ∈ s, t i).Finite - Set.Finite.iUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set ι} (ht : t.Finite) (hs : ∀ i ∈ t, (s i).Finite) (he : ∀ i ∉ t, s i = ∅) : (⋃ i, s i).Finite - Set.Finite.biUnion' 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type u_1} {s : Set ι} (hs : s.Finite) {t : (i : ι) → i ∈ s → Set α} (ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite) : (⋃ i, ⋃ (h : i ∈ s), t i h).Finite - DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u_1} {c : Set (Set α)} (hn : c.Nonempty) (hc : DirectedOn (fun x1 x2 => x1 ⊆ x2) c) {s : Set α} (hs : s.Finite) (hsc : s ⊆ ⋃₀ c) : ∃ t ∈ c, s ⊆ t - Set.finite_subset_iUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {s : Set α} (hs : s.Finite) {ι : Type u_1} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) : ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i - Set.Finite.bddAbove_biUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} [Preorder α] [IsDirectedOrder α] [Nonempty α] {I : Set β} {S : β → Set α} (H : I.Finite) : BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) - Set.Finite.bddBelow_biUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} [Preorder α] [IsCodirectedOrder α] [Nonempty α] {I : Set β} {S : β → Set α} (H : I.Finite) : BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i) - Set.finite_iUnion_iff 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type u_1} {s : ι → Set α} (hs : Pairwise fun i j => Disjoint (s i) (s j)) : (⋃ i, s i).Finite ↔ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite - Set.finite_diff_iUnion_Ioo 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y).Finite - Set.finite_sdiff_iUnion_Ioo 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y).Finite - Set.finite_diff_iUnion_Ioo' 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ x, Set.Ioo ↑x.1 ↑x.2).Finite - Set.finite_sdiff_iUnion_Ioo' 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} [LinearOrder α] (s : Set α) : (s \ ⋃ x, Set.Ioo ↑x.1 ↑x.2).Finite - Set.iUnion_pi_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type u_3} {I : Set ι} {s : (i : ι) → ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) : (⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j - Set.PairwiseDisjoint.finite_biUnion_iff 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {β : Type v} {f : β → Set α} {s : Set β} (hs : s.PairwiseDisjoint f) : (⋃ i ∈ s, f i).Finite ↔ (∀ i ∈ s, (f i).Finite) ∧ {i | i ∈ s ∧ (f i).Nonempty}.Finite - Set.Finite.biInf_iSup_eq 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : (a : ι) → κ a → α} : ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a) - Set.Finite.biSup_iInf_eq 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : (a : ι) → κ a → α} : ⨆ a ∈ s, ⨅ b, f a b = ⨅ g, ⨆ a ∈ s, f a (g a) - Set.Finite.iInf_biSup_of_antitone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι'] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j - Set.Finite.iInf_biSup_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι'] [Order.Coframe α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) : ⨅ j, ⨆ i ∈ s, f i j = ⨆ i ∈ s, ⨅ j, f i j - Set.Finite.iSup_biInf_of_antitone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι'] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Antitone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j - Set.Finite.iSup_biInf_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι'] [Order.Frame α] {s : Set ι} (hs : s.Finite) {f : ι → ι' → α} (hf : ∀ i ∈ s, Monotone (f i)) : ⨆ j, ⨅ i ∈ s, f i j = ⨅ i ∈ s, ⨆ j, f i j - Set.eq_finite_iUnion_of_finite_subset_iUnion 📋 Mathlib.Data.Set.Finite.Lattice
{α : Type u} {ι : Type u_1} {s : ι → Set α} {t : Set α} (tfin : t.Finite) (h : t ⊆ ⋃ i, s i) : ∃ I, I.Finite ∧ ∃ σ, (∀ (i : ↑{i | i ∈ I}), (σ i).Finite) ∧ (∀ (i : ↑{i | i ∈ I}), σ i ⊆ s ↑i) ∧ t = ⋃ i, σ i
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"somewhere in their lemma name.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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis not the last.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 ce5dd8c