Lax Lean Archive

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

Mixed proof: one sibling and one foreign assumption

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

    Statement 2 is proved from statement 1 of this concept and from statement 3 of SiblingConclusionRightSiblingConclusionRight. One assumption arrow is local, the other crosses to another concept box, so the drawing has to place a turnstile that is a sibling proof on one side and a cross-concept proof on the other.

    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 s1 proven

    2 s2 proven

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2import Lax771644.Foundations
    3
    4/-!
    5---
    6title: Mixed proof: one sibling and one foreign assumption
    7type: theorem
    8---
    9Statement 2 is proved from statement 1 of this concept *and* from statement 3
    10of `SiblingConclusionRight`. One assumption arrow is local, the other crosses to
    11another concept box, so the drawing has to place a turnstile that is a sibling
    12proof on one side and a cross-concept proof on the other.
    13
    14# Formalization notes
    15
    16The foreign rung 12→1012 \to 10 picks up exactly where the local rung
    1742→4042 \to 40 leaves off, after a free weakening from stage 40 to stage 12.
    18-/
    19
    20namespace Lax771644.MixedSiblingAndForeign
    21
    22/-- Descent from stage 42 to stage 40. -/
    23axiom s1 : Foundations.Descent 42 40
    24
    25/-- Descent from stage 42 all the way down to stage 10. -/
    26axiom s2 : Foundations.Descent 42 10
    27
    28end Lax771644.MixedSiblingAndForeign
    29
    Show ProofShow Proof
    Formalization notes

    The foreign rung 12→1012 \to 10 picks up exactly where the local rung 42→4042 \to 40 leaves off, after a free weakening from stage 40 to stage 12.

    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…