Loogle!

Result

Found 42 declarations mentioning Std.PRange.UpwardEnumerable.Map.

Std.PRange.UpwardEnumerable.Map 📋 Init.Data.Range.Polymorphic.Map
(α : Type u) (β : Type v) [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] : Type (max u v)
Std.PRange.UpwardEnumerable.Map.toFun 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (self : Std.PRange.UpwardEnumerable.Map α β) : α → β
Std.PRange.UpwardEnumerable.Map.PreservesLE 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LE β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.UpwardEnumerable.Map.PreservesLT 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LT α] [LT β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.UpwardEnumerable.Map.PreservesLeast? 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.PRange.Least? α] [Std.PRange.Least? β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxc.HasSize α] [Std.Rxc.HasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxi.HasSize α] [Std.Rxi.HasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxo.HasSize α] [Std.Rxo.HasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) : Prop
Std.PRange.LawfulUpwardEnumerable.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_2} {β : Type u_1} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.PRange.LawfulUpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) : Std.PRange.LawfulUpwardEnumerable α
Std.Rxi.IsAlwaysFinite.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_2} {β : Type u_1} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxi.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β) : Std.Rxi.IsAlwaysFinite α
Std.PRange.UpwardEnumerable.Map.injective 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (self : Std.PRange.UpwardEnumerable.Map α β) : Function.Injective self.toFun
Std.PRange.LawfulUpwardEnumerableLE.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LE β] [Std.PRange.LawfulUpwardEnumerableLE β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE] : Std.PRange.LawfulUpwardEnumerableLE α
Std.PRange.LawfulUpwardEnumerableLT.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LT α] [LT β] [Std.PRange.LawfulUpwardEnumerableLT β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLT] : Std.PRange.LawfulUpwardEnumerableLT α
Std.PRange.LawfulUpwardEnumerableLeast?.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.PRange.Least? α] [Std.PRange.Least? β] [Std.PRange.LawfulUpwardEnumerableLeast? β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLeast?] : Std.PRange.LawfulUpwardEnumerableLeast? α
Std.Rxc.IsAlwaysFinite.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LE β] [Std.Rxc.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE] : Std.Rxc.IsAlwaysFinite α
Std.Rxi.LawfulHasSize.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxi.HasSize α] [Std.Rxi.HasSize β] [Std.Rxi.LawfulHasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesRxiSize] : Std.Rxi.LawfulHasSize α
Std.Rxo.IsAlwaysFinite.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LT α] [LT β] [Std.Rxo.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLT] : Std.Rxo.IsAlwaysFinite α
Std.PRange.UpwardEnumerable.Map.le_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α} : Std.PRange.UpwardEnumerable.LE a b ↔ Std.PRange.UpwardEnumerable.LE (f.toFun a) (f.toFun b)
Std.PRange.UpwardEnumerable.Map.lt_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α} : Std.PRange.UpwardEnumerable.LT a b ↔ Std.PRange.UpwardEnumerable.LT (f.toFun a) (f.toFun b)
Std.PRange.UpwardEnumerable.Map.succ?_eq_none_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) {a : α} : Std.PRange.succ? a = none ↔ Std.PRange.succ? (f.toFun a) = none
Std.PRange.UpwardEnumerable.Map.succ?_toFun 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (self : Std.PRange.UpwardEnumerable.Map α β) (a : α) : Std.PRange.succ? (self.toFun a) = Option.map self.toFun (Std.PRange.succ? a)
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxi.HasSize α] [Std.Rxi.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β} (size_eq : ∀ {b : α}, Std.Rxi.HasSize.size b = Std.Rxi.HasSize.size (f.toFun b)) : f.PreservesRxiSize
Std.PRange.UpwardEnumerable.Map.PreservesRxiSize.size_eq 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : Std.Rxi.HasSize α} {inst✝³ : Std.Rxi.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesRxiSize] {b : α} : Std.Rxi.HasSize.size b = Std.Rxi.HasSize.size (f.toFun b)
Std.PRange.UpwardEnumerable.Map.succMany?_toFun 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (self : Std.PRange.UpwardEnumerable.Map α β) (n : ℕ) (a : α) : Std.PRange.succMany? n (self.toFun a) = Option.map self.toFun (Std.PRange.succMany? n a)
Std.PRange.UpwardEnumerable.Map.PreservesLeast?.map_least? 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : Std.PRange.Least? α} {inst✝³ : Std.PRange.Least? β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesLeast?] : Option.map f.toFun Std.PRange.least? = Std.PRange.least?
Std.PRange.UpwardEnumerable.Map.PreservesLeast?.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.PRange.Least? α] [Std.PRange.Least? β] {f : Std.PRange.UpwardEnumerable.Map α β} (map_least? : Option.map f.toFun Std.PRange.least? = Std.PRange.least?) : f.PreservesLeast?
Std.PRange.instPreservesLTOfLawfulOrderLTOfPreservesLE 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LT α] [Std.LawfulOrderLT α] [LE β] [LT β] [Std.LawfulOrderLT β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE] : f.PreservesLT
Std.Rxc.LawfulHasSize.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LE β] [Std.Rxc.HasSize α] [Std.Rxc.HasSize β] [Std.Rxc.LawfulHasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLE] [f.PreservesRxcSize] : Std.Rxc.LawfulHasSize α
Std.Rxo.LawfulHasSize.ofMap 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LT α] [LT β] [Std.Rxo.HasSize α] [Std.Rxo.HasSize β] [Std.Rxo.LawfulHasSize β] (f : Std.PRange.UpwardEnumerable.Map α β) [f.PreservesLT] [f.PreservesRxoSize] : Std.Rxo.LawfulHasSize α
Std.PRange.UpwardEnumerable.Map.succ?_eq_some_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) {a b : α} : Std.PRange.succ? a = some b ↔ Std.PRange.succ? (f.toFun a) = some (f.toFun b)
Std.PRange.UpwardEnumerable.Map.succ?_toFun' 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (f : Std.PRange.UpwardEnumerable.Map α β) : Std.PRange.succ? ∘ f.toFun = Option.map f.toFun ∘ Std.PRange.succ?
Std.PRange.UpwardEnumerable.Map.PreservesLE.le_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : LE α} {inst✝³ : LE β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesLE] {a b : α} : a ≤ b ↔ f.toFun a ≤ f.toFun b
Std.PRange.UpwardEnumerable.Map.PreservesLE.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LE α] [LE β] {f : Std.PRange.UpwardEnumerable.Map α β} (le_iff : ∀ {a b : α}, a ≤ b ↔ f.toFun a ≤ f.toFun b) : f.PreservesLE
Std.PRange.UpwardEnumerable.Map.PreservesLT.lt_iff 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : LT α} {inst✝³ : LT β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesLT] {a b : α} : a < b ↔ f.toFun a < f.toFun b
Std.PRange.UpwardEnumerable.Map.PreservesLT.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [LT α] [LT β] {f : Std.PRange.UpwardEnumerable.Map α β} (lt_iff : ∀ {a b : α}, a < b ↔ f.toFun a < f.toFun b) : f.PreservesLT
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxc.HasSize α] [Std.Rxc.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β} (size_eq : ∀ {a b : α}, Std.Rxc.HasSize.size a b = Std.Rxc.HasSize.size (f.toFun a) (f.toFun b)) : f.PreservesRxcSize
Std.PRange.UpwardEnumerable.Map.PreservesRxcSize.size_eq 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : Std.Rxc.HasSize α} {inst✝³ : Std.Rxc.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesRxcSize] {a b : α} : Std.Rxc.HasSize.size a b = Std.Rxc.HasSize.size (f.toFun a) (f.toFun b)
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [Std.Rxo.HasSize α] [Std.Rxo.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β} (size_eq : ∀ {a b : α}, Std.Rxo.HasSize.size a b = Std.Rxo.HasSize.size (f.toFun a) (f.toFun b)) : f.PreservesRxoSize
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize.size_eq 📋 Init.Data.Range.Polymorphic.Map
{α : Type u_1} {β : Type u_2} {inst✝ : Std.PRange.UpwardEnumerable α} {inst✝¹ : Std.PRange.UpwardEnumerable β} {inst✝² : Std.Rxo.HasSize α} {inst✝³ : Std.Rxo.HasSize β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesRxoSize] {a b : α} : Std.Rxo.HasSize.size a b = Std.Rxo.HasSize.size (f.toFun a) (f.toFun b)
Std.PRange.UpwardEnumerable.Map.mk 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (toFun : α → β) (injective : Function.Injective toFun) (succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a)) (succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)) : Std.PRange.UpwardEnumerable.Map α β
Std.PRange.UpwardEnumerable.Map.mk.sizeOf_spec 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] [SizeOf α] [SizeOf β] (toFun : α → β) (injective : Function.Injective toFun) (succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a)) (succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)) : sizeOf { toFun := toFun, injective := injective, succ?_toFun := succ?_toFun, succMany?_toFun := succMany?_toFun } = 1
Std.PRange.UpwardEnumerable.Map.mk.injEq 📋 Init.Data.Range.Polymorphic.Map
{α : Type u} {β : Type v} [Std.PRange.UpwardEnumerable α] [Std.PRange.UpwardEnumerable β] (toFun : α → β) (injective : Function.Injective toFun) (succ?_toFun : ∀ (a : α), Std.PRange.succ? (toFun a) = Option.map toFun (Std.PRange.succ? a)) (succMany?_toFun : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun a) = Option.map toFun (Std.PRange.succMany? n a)) (toFun✝ : α → β) (injective✝ : Function.Injective toFun✝) (succ?_toFun✝ : ∀ (a : α), Std.PRange.succ? (toFun✝ a) = Option.map toFun✝ (Std.PRange.succ? a)) (succMany?_toFun✝ : ∀ (n : ℕ) (a : α), Std.PRange.succMany? n (toFun✝ a) = Option.map toFun✝ (Std.PRange.succMany? n a)) : ({ toFun := toFun, injective := injective, succ?_toFun := succ?_toFun, succMany?_toFun := succMany?_toFun } = { toFun := toFun✝, injective := injective✝, succ?_toFun := succ?_toFun✝, succMany?_toFun := succMany?_toFun✝ }) = (toFun = toFun✝)

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:

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 ?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
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 36960b0 serving mathlib revision 9a4cf1d