Lax Lean Archive

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

Isolated island (no statements, no uses)

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

definition

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

    Definition

    A definition-concept that declares no statement, imports no other concept of this submission, and is imported by none. It is here to check that the drawing places a concept with no incident edge at all.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2
    3/-!
    4---
    5title: Isolated island (no statements, no uses)
    6type: definition
    7---
    8A definition-concept that declares no statement, imports no other concept of
    9this submission, and is imported by none. It is here to check that the drawing
    10places a concept with no incident edge at all.
    11
    12# Formalization notes
    13
    14The marker predicate is never used anywhere. Its only purpose is to give
    15this module a declaration so that it is a concept rather than an empty file.
    16-/
    17
    18namespace Lax771644.IsolatedIsland
    19
    20/-- A marker predicate that nothing in this submission ever mentions. -/
    21def marker : Prop := ∀ n : ℕ, n = n
    22
    23end Lax771644.IsolatedIsland
    24
    Formalization notes

    The marker predicate is never used anywhere. Its only purpose is to give this module a declaration so that it is a concept rather than an empty file.

    Builds on

    none

    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…