Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Ünïcode: μ\mu-descent and ε\varepsilon–δ\delta weakening (ℵ₀ rungs, ∀∃, 中文)

Lax771644.UnicodeNames · concepts/Lax771644/UnicodeNames.lean · lax-771644

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A concept whose title and whose statement names carry non-ASCII characters, to check that the figure's labels, tooltips and anchors survive them. The Greek letters have no mathematical meaning here.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 εδ_descent proven

    2 μ_descent proven

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2import Lax771644.Foundations
    3
    4/-!
    5---
    6title: Ünïcode: μ\mu-descent and ε\varepsilon–δ\delta weakening (ℵ₀ rungs, ∀∃, 中文)
    7type: theorem
    8---
    9A concept whose title and whose statement names carry non-ASCII characters, to
    10check that the figure's labels, tooltips and anchors survive them. The Greek
    11letters have no mathematical meaning here.
    12
    13# Formalization notes
    14
    15`εδ_descent` sorts before `μ_descent` by code point, so the concept-named
    16docks come out in the order ε, μ and the sibling proof again has its conclusion
    17on the left.
    18-/
    19
    20namespace Lax771644.UnicodeNames
    21
    22/-- Descent from stage 610 to stage 608. -/
    23axiom εδ_descent : Foundations.Descent 610 608
    24
    25/-- Descent from stage 610 to stage 609. -/
    26axiom μ_descent : Foundations.Descent 610 609
    27
    28end Lax771644.UnicodeNames
    29
    Show ProofShow Proof
    Formalization notes

    εδdescentεδ_descent sorts before μdescentμ_descent by code point, so the concept-named docks come out in the order ε, μ and the sibling proof again has its conclusion on the left.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…