Lax Lean Archive

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

Rooted forests through ancestor relations

Lax183560.AncestorForest · concepts/Lax183560/AncestorForest.lean · lax-183560

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 strict ancestor relation of a rooted forest is transitive and irreflexive, and the ancestors of each vertex are linearly ordered. On a finite vertex set, these conditions characterize the strict ancestor relations of rooted forests.

    Concept map
    1 concept; 1 descendant hidden
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Rooted forests through ancestor relations
    6type: definition
    7---
    8A strict ancestor relation of a rooted forest is transitive and irreflexive,
    9and the ancestors of each vertex are linearly ordered. On a finite vertex
    10set, these conditions characterize the strict ancestor relations of rooted
    11forests.
    12-/
    13
    14namespace Lax183560.AncestorForest
    15
    16/-- A strict ancestor relation of a rooted forest on `V`. -/
    17structure AncestorForest (V : Type) where
    18 ancestor : V → V → Prop
    19 transitive : IsTrans V ancestor
    20 irreflexive : Std.Irrefl ancestor
    21 ancestors_linearly_ordered : ∀ u v w : V,
    22 (ancestor u w ∧ ancestor v w) → (u = v ∨ ancestor u v ∨ ancestor v u)
    23
    24
    25end Lax183560.AncestorForest
    26
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…