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 22 research declarations. Search 10,000 more complete Mathlib declarations.
22 results
Clear filtersRelMfld.SatisfiesHPrincipleWith.bs
Plain-language statement
If a relation satisfies the parametric relative C⁰-dense h-principle wrt some data then we can forget the homotopy and get a family of solutions from every family of formal solutions.
Source project: Sphere eversion
Person-level attribution pending.
sfHomotopy_in'
Plain-language statement
A more precise version of sfHomotopy_in.
Source project: Sphere eversion
Person-level attribution pending.
SmoothSurroundingFamily.eventually_exists_surroundingPts_approxSurroundingPointsAt
Plain-language statement
The key property from which it should be easy to construct localCenteringDensity, localCenteringDensityNhd etc below.
Source project: Sphere eversion
Person-level attribution pending.
surroundingFamilyIn_iff_germ
Project documentation
A more precise version of sfHomotopy_in. -/ theorem sfHomotopy_in' {ι} (h₀ : SurroundingFamily g b γ₀ U) (h₁ : SurroundingFamily g b γ₁ U) (τ : ι → ℝ) (x : ι → E) (i : ι) {V : Set E} (hx : x i ∈ V) {t : ℝ} (ht : t ∈ I) {s : ℝ} (h_in₀ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠ 1 → (x i, γ₀ (x i) t s) ∈ Ω) (h_in₁ : ∀ i, x i ∈ V → ∀ t ∈ I, ∀ (s : ℝ), τ i ≠...
Source project: Sphere eversion
Person-level attribution pending.