Lax Lean Archive

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

A statement whose name is its concept's name

Lax771644.WholeConceptAssumption · concepts/Lax771644/WholeConceptAssumption.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

    This concept declares one statement named exactly like the concept module itself, alongside an ordinary numbered sibling. It is the closest the format comes to a whole-concept assumption: a proof assuming it names the concept id rather than a name below it.

    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 Lax771644.WholeConceptAssumption proven

    2 s2 proven

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2import Lax771644.Foundations
    3
    4/-!
    5---
    6title: A statement whose name is its concept's name
    7type: theorem
    8---
    9This concept declares one statement named exactly like the concept module
    10itself, alongside an ordinary numbered sibling. It is the closest the format
    11comes to a *whole-concept* assumption: a proof assuming it names the concept id
    12rather than a name below it.
    13
    14# Formalization notes
    15
    16Lean is happy to have a constant `Lax771644.WholeConceptAssumption` and a
    17constant `Lax771644.WholeConceptAssumption.s2` at the same time, exactly as it
    18has `Nat` and `Nat.succ`. The archive treats the first as an ordinary statement
    19of the module it originates in, so its identifier collides with the concept's
    20own identifier — which is the edge case this module exists to pin down.
    21-/
    22
    23namespace Lax771644
    24
    25/-- Descent from stage 320 to stage 319, declared with the concept's own name. -/
    26axiom WholeConceptAssumption : Foundations.Descent 320 319
    27
    28end Lax771644
    29
    30namespace Lax771644.WholeConceptAssumption
    31
    32/-- Descent from stage 320 to stage 318. -/
    33axiom s2 : Foundations.Descent 320 318
    34
    35end Lax771644.WholeConceptAssumption
    36
    Show ProofShow Proof
    Formalization notes

    Lean is happy to have a constant Lax771644.WholeConceptAssumptionLax771644.WholeConceptAssumption and a constant Lax771644.WholeConceptAssumption.s2Lax771644.WholeConceptAssumption.s2 at the same time, exactly as it has NatNat and Nat.succNat.succ. The archive treats the first as an ordinary statement of the module it originates in, so its identifier collides with the concept's own identifier — which is the edge case this module exists to pin down.

    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…