Loogle!

Result

Found 715 declarations mentioning LE.le and Max.max. Of these, 18 match your pattern(s).

• sup_le_sup_left 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a ≤ b) (c : α) : c ⊔ a ≤ c ⊔ b
• sup_le_sup_right 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a ≤ b) (c : α) : a ⊔ c ≤ b ⊔ c
• sup_le_sup 📋 Mathlib.Order.Lattice
  {α : Type u} [SemilatticeSup α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d
• le_of_inf_le_sup_le 📋 Mathlib.Order.Lattice
  {α : Type u} [DistribLattice α] {x y z : α} (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y
• sdiff_le_sdiff_of_sup_le_sup_left 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} (h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c
• sdiff_le_sdiff_of_sup_le_sup_right 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c
• max_le_max_left 📋 Mathlib.Order.MinMax
  {α : Type u} [LinearOrder α] {a b : α} (c : α) (h : a ≤ b) : max c a ≤ max c b
• max_le_max_right 📋 Mathlib.Order.MinMax
  {α : Type u} [LinearOrder α] {a b : α} (c : α) (h : a ≤ b) : max a c ≤ max b c
• max_le_max 📋 Mathlib.Order.MinMax
  {α : Type u} [LinearOrder α] {a b c d : α} : a ≤ c → b ≤ d → max a b ≤ max c d
• Set.uIcc_subset_uIcc_iff_le' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
• Set.uIcc_subset_uIcc_iff_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
• AddSubgroup.map_le_map_iff' 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
• Subgroup.map_le_map_iff' 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : Subgroup.map f H ≤ Subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
• Finset.uIcc_subset_uIcc_iff_le' 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
• Finset.uIcc_subset_uIcc_iff_le 📋 Mathlib.Order.Interval.Finset.Basic
  {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
• inf_lt_inf_of_lt_of_sup_le_sup 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : x < y) (hinf : y ⊔ z ≤ x ⊔ z) : x ⊓ z < y ⊓ z
• eq_of_le_of_inf_le_of_sup_le 📋 Mathlib.Order.ModularLattice
  {α : Type u_1} [Lattice α] [IsModularLattice α] {x y z : α} (hxy : x ≤ y) (hinf : y ⊓ z ≤ x ⊓ z) (hsup : y ⊔ z ≤ x ⊔ z) : x = y
• NumberField.Units.regOfFamily_div_regOfFamily 📋 Mathlib.NumberTheory.NumberField.Units.Regulator
  {K : Type u_1} [Field K] [NumberField K] {u v : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hv : NumberField.Units.IsMaxRank v) (h : Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K ≤ Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K) : NumberField.Units.regOfFamily u / NumberField.Units.regOfFamily v = ↑((Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K))

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 7379a9f