Loogle!
Result
Found 7953 definitions mentioning HSub.hSub. Of these, 211 have a name containing "tsub". Of these, 14 match your pattern(s).
- tsub_tsub_le Mathlib.Algebra.Order.Sub.Defs
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α}, b - (b - a) ≤ a - tsub_tsub_tsub_le_tsub Mathlib.Algebra.Order.Sub.Defs
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α} [inst_4 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], c - a - (c - b) ≤ b - a - tsub_tsub_le_tsub_add Mathlib.Algebra.Order.Sub.Defs
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] [inst_4 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] {a b c : α}, a - (b - c) ≤ a - b + c - tsub_tsub_tsub_cancel_right Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst : OrderedSub α] {a b c : α}, c ≤ b → a - c - (b - c) = a - b - AddLECancellable.tsub_tsub_cancel_of_le Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b : α}, AddLECancellable (b - a) → a ≤ b → b - (b - a) = a - tsub_tsub_cancel_of_le Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b : α} [inst : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], a ≤ b → b - (b - a) = a - AddLECancellable.tsub_tsub_tsub_cancel_left Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α}, AddLECancellable (a - b) → b ≤ a → a - c - (a - b) = b - c - tsub_tsub_tsub_cancel_left Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α} [inst : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], b ≤ a → a - c - (a - b) = b - c - AddLECancellable.add_tsub_tsub_cancel Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α}, AddLECancellable (a - c) → c ≤ a → a + b - (a - c) = b + c - tsub_tsub_eq_add_tsub_of_le Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α} [inst_6 : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], c ≤ b → a - (b - c) = a + c - b - AddLECancellable.tsub_tsub_assoc Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α}, AddLECancellable (b - c) → b ≤ a → c ≤ b → a - (b - c) = a - b + c - add_tsub_tsub_cancel Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α} [inst_6 : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], c ≤ a → a + b - (a - c) = b + c - tsub_tsub_assoc Mathlib.Algebra.Order.Sub.Unbundled.Basic
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α] [inst_3 : CovariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] [inst_4 : Sub α] [inst_5 : OrderedSub α] {a b c : α} [inst_6 : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2], b ≤ a → c ≤ b → a - (b - c) = a - b + c - tsub_tsub_eq_min Mathlib.Algebra.Order.Sub.Basic
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] [inst_3 : ContravariantClass α α (fun x1 x2 => x1 + x2) fun x1 x2 => x1 ≤ x2] (a b : α), a - (a - b) = min a b
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try 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 findtsum_lt_tsum
even though the hypothesisf 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 f46663a
serving mathlib revision fb1cb21