Lax Lean Archive

Least fixed points on finite relations

Lax751879.LeastFixedPoints · concepts/Lax751879/LeastFixedPoints.lean · lax-751879

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

    Definition and theorem

    For a monotone operator FF on sets, its least fixed point is the intersection of all sets RR satisfying F(R)⊆RF(R)\subseteq R. Starting from the empty set, iterate FF. On a finite set of NN possible elements, stage NN is already the least fixed point. For a kk-ary relation on an nn-element universe, there are nkn^k possible tuples.

    The intersection definition is total even for nonmonotone operators; the fixed-point and convergence statements explicitly require monotonicity.

    Concept map
    1 concept; 3 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 finiteConvergence proven

    2 fixedPoint proven

    3 least proven

    Lean source view on GitHub

    1import Mathlib.Data.Set.Lattice
    2import Mathlib.Data.Fintype.Card
    3
    4/-!
    5---
    6title: Least fixed points on finite relations
    7type: definition and theorem
    8---
    9For a monotone operator FF on sets, its least fixed point is the intersection
    10of all sets RR satisfying F(R)⊆RF(R)\subseteq R. Starting from the empty set,
    11iterate FF. On a finite set of NN possible elements, stage NN is already
    12the least fixed point. For a kk-ary relation on an nn-element universe,
    13there are nkn^k possible tuples.
    14
    15The intersection definition is total even for nonmonotone operators; the
    16fixed-point and convergence statements explicitly require monotonicity.
    17-/
    18
    19namespace Lax751879.LeastFixedPoints
    20
    21def leastFixedPoint {α : Type} (F : Set α → Set α) : Set α :=
    22 sInf {R | F R ⊆ R}
    23
    24def stage {α : Type} (F : Set α → Set α) : Nat → Set α
    25 | 0 => ∅
    26 | t + 1 => F (stage F t)
    27
    28axiom fixedPoint {α : Type} (F : Set α → Set α) (hF : Monotone F) :
    29 F (leastFixedPoint F) = leastFixedPoint F
    30
    31axiom least {α : Type} (F : Set α → Set α) (R : Set α)
    32 (hR : F R ⊆ R) : leastFixedPoint F ⊆ R
    33
    34axiom finiteConvergence {α : Type} [Fintype α]
    35 (F : Set α → Set α) (hF : Monotone F) :
    36 stage F (Fintype.card α) = leastFixedPoint F
    37
    38end Lax751879.LeastFixedPoints
    39
    Show ProofShow ProofShow Proof
    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…