Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax979537.LeastFixedPoints

Least fixed points on finite relations

concepts/Lax979537/LeastFixedPoints.lean · lax-979537

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.

    Concept map

    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.

    1st statement finiteConvergence proven

    2nd statement fixedPoint proven

    3rd statement least proven

    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.

    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 Lax979537.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 Lax979537.LeastFixedPoints
    39
    Show ProofShow ProofShow Proof

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…