def Fixpoint.CoindPred {α : Type u_1} (F : (α → Prop) → α → Prop) : α → Prop

Equations

• Fixpoint.CoindPred F = Fixpoint.supPostfix F

def Fixpoint.CoindPredOrFn {α : Type u_1} (F : (α → Prop) → α → Prop) (p : α → Prop) : α → Prop

Equations

• Fixpoint.CoindPredOrFn F p = F fun (x : α) => Fixpoint.CoindPred F x ∨ p x

def Fixpoint.CoindPredOr {α : Type u_1} (F : (α → Prop) → α → Prop) : α → Prop

Equations

• Fixpoint.CoindPredOr F = Fixpoint.CoindPred (Fixpoint.CoindPredOrFn F)

theorem Fixpoint.CoindPred.ctor {α : Type u_1} {F : (α → Prop) → α → Prop} {x : α} (hf : Monotone F) (h : F (CoindPred F) x) : CoindPred F x

theorem Fixpoint.CoindPred.cases' {α : Type u_1} {F : (α → Prop) → α → Prop} {x : α} (hf : Monotone F) (h : CoindPred F x) : F (CoindPred F) x

theorem Fixpoint.CoindPred.cases {α : Type u_1} {F : (α → Prop) → α → Prop} {x : α} {P : Prop} (hf : Monotone F) (h₁ : CoindPred F x) (h₂ : F (CoindPred F) x → P) : P

theorem Fixpoint.apply_coindPred_eq {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : F (CoindPred F) = CoindPred F

theorem Fixpoint.CoindPred.coind' {α : Type u_1} {F : (α → Prop) → α → Prop} {p : α → Prop} {x : α} (hf : Monotone F) (h₁ : p x) (h₂ : ∀ ⦃y : α⦄, p y → F p y) : CoindPred F x

theorem Fixpoint.monotone_coindPredOrFn {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : Monotone (CoindPredOrFn F)

theorem Fixpoint.coindPred_le_coindPredOr {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : CoindPred F ≤ CoindPredOr F

theorem Fixpoint.coindPredOr_eq_coindPred {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : CoindPredOr F = CoindPred F

theorem Fixpoint.CoindPred.coind {α : Type u_1} {F : (α → Prop) → α → Prop} {p : α → Prop} {x : α} (hf : Monotone F) (h₁ : p x) (h₂ : ∀ ⦃y : α⦄, p y → F p y) : CoindPredOr F x