def Fixpoint.infPrefix {α : Type u_1} [LE α] [InfSet α] (f : α → α) : α

Equations

• Fixpoint.infPrefix f = sInf (Set.ofPred (Fixpoint.PreFixpoint f))

def Fixpoint.supPostfix {α : Type u_1} [LE α] [SupSet α] (f : α → α) : α

Equations

• Fixpoint.supPostfix f = sSup (Set.ofPred (Fixpoint.PostFixpoint f))

theorem Fixpoint.preFixpoint_infPrefix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : PreFixpoint f (infPrefix f)

theorem Fixpoint.postFixpoint_supPostfix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : PostFixpoint f (supPostfix f)

theorem Fixpoint.postFixpoint_infPrefix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : PostFixpoint f (infPrefix f)

theorem Fixpoint.preFixpoint_supPostfix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : PreFixpoint f (supPostfix f)

theorem Fixpoint.fixpoint_infPrefix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : Fixpoint f (infPrefix f)

theorem Fixpoint.fixpoint_supPostfix {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (hf : Monotone f) : Fixpoint f (supPostfix f)

theorem Fixpoint.le_of_preFixpoint_infPrefix {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] (h : PreFixpoint f x) : infPrefix f ≤ x

theorem Fixpoint.le_of_postFixpoint_supPostfix {α : Type u_1} {f : α → α} {x : α} [ha : CompleteLattice α] (h : PostFixpoint f x) : x ≤ supPostfix f

theorem Fixpoint.exi_least_fixpoint_of_monotone {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (h : Monotone f) : ∃ (x : α), Fixpoint f x ∧ ∀ (y : α), Fixpoint f y → x ≤ y

theorem Fixpoint.exi_greatest_fixpoint_of_monotone {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (h : Monotone f) : ∃ (x : α), Fixpoint f x ∧ ∀ (y : α), Fixpoint f y → y ≤ x

theorem Fixpoint.exi_least_and_greatest_fixpoint_of_monotone {α : Type u_1} {f : α → α} [ha : CompleteLattice α] (h : Monotone f) : (∃ (x : α), Fixpoint f x ∧ ∀ (y : α), Fixpoint f y → x ≤ y) ∧ ∃ (x : α), Fixpoint f x ∧ ∀ (y : α), Fixpoint f y → y ≤ x

theorem Fixpoint.postFixpoint_least_preFixpoint {α : Type u_1} {f : α → α} {x : α} [ha : PartialOrder α] (hf : Monotone f) (h₁ : PreFixpoint f x) (h₂ : ∀ ⦃y : α⦄, PreFixpoint f y → x ≤ y) : PostFixpoint f x

theorem Fixpoint.preFixpoint_greatest_postFixpoint {α : Type u_1} {f : α → α} {x : α} [ha : PartialOrder α] (hf : Monotone f) (h₁ : PostFixpoint f x) (h₂ : ∀ ⦃y : α⦄, PostFixpoint f y → y ≤ x) : PreFixpoint f x

@[simp]

theorem Fixpoint.infPrefix_pi_const {α : Type u_1} {P : Prop} : (infPrefix fun (x : α → Prop) (x_1 : α) => P) = fun (x : α) => P

@[simp]

theorem Fixpoint.supPostfix_pi_const {α : Type u_1} {P : Prop} : (supPostfix fun (x : α → Prop) (x_1 : α) => P) = fun (x : α) => P