@[reducible, inline]

abbrev DY.Fixpoint.Set (α : Type u) : Type u

Equations

• DY.Fixpoint.Set α = (α → Prop)

def DY.Fixpoint.IsMonotonic {α : Type u} (f : Set α → Set α) : Prop

Equations

• DY.Fixpoint.IsMonotonic f = ∀ (set1 set2 : DY.Fixpoint.Set α), (∀ (x : α), set1 x → set2 x) → ∀ (x : α), f set1 x → f set2 x

def DY.Fixpoint.combine {α : Type u} {Id : Type} (fs : Id → Set α → Set α) (set : Set α) : Set α

Equations

• DY.Fixpoint.combine fs set x = ∃ (id : Id), fs id set x

theorem DY.Fixpoint.combine_isMonotonic {α : Type u} {Id : Type} (fs : Id → Set α → Set α) (h_fs : ∀ (id : Id), IsMonotonic (fs id)) : IsMonotonic (combine fs)

def DY.Fixpoint.mkLeastFixpoint {α : Type u} (f : Set α → Set α) : Set α

Equations

• DY.Fixpoint.mkLeastFixpoint f x = ∀ (s : DY.Fixpoint.Set α), f s ⊆ s → s x

theorem DY.Fixpoint.mkLeastFixpoint_is_fixpoint {α : Type u} (f : Set α → Set α) (h_mono : IsMonotonic f) : f (mkLeastFixpoint f) = mkLeastFixpoint f

theorem DY.Fixpoint.mkLeastFixpoint_is_least {α : Type u} (f : Set α → Set α) : IsMonotonic f → ∀ (set : Set α), (∀ (x : α), f set x → set x) → ∀ (x : α), mkLeastFixpoint f x → set x