Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,621 to 1,626 of 2,569 results.
LO.FirstOrder.Semiterm.stepVec_ofFn
Mathematical statement
With every lookup present and non-zero, the fold rebuilds the vecToNat code of the arguments.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.SetTheory.replacement_rel_existsUnique_of_mem_existsUnique
Project documentation
A stronger variant of (unique existence of) replacement, which only requires uniqueness on X. The statement of this lemma is thanks to tosiaki.
Source project: Foundation
Person-level attribution pending.
LO.FirstOrder.SetTheory.restrict_insert_kpair_eq_restrict_of_not_mem
Mathematical statement
Restricting an inserted relation to a set that does not contain the inserted first coordinate recovers the original restriction.
Source project: Foundation
Person-level attribution pending.
local_loops
Project documentation
Note: The conditions in this lemma are currently a bit weaker than the ones mentioned in the blueprint. TODO: use local_loops_def
Source project: Sphere eversion
Person-level attribution pending.
localisation_stability
Mathematical statement
Lemma lem:localisation_stability.
Source project: Sphere eversion
Person-level attribution pending.
log_le_const_mul_pow
Project documentation
The union of B-sets used in the proof of proposition 2.6. -/ noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ)) := (indexSet' α β γ d x ε).sup fun ⟨r, s, t, c⟩ ↦ B_finset d c (fun i ↦ 2^r i) (fun i ↦ 2^s i) (fun i ↦ 2^t i) theorem similar_pow_log {x : ℕ} (hx : 0 < x) : x ~ 2 ^ Na...
Source project: ABC Exceptions
Person-level attribution pending.