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

Equations

• Fixpoint.IndPred F = Fixpoint.infPrefix F

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

Equations

• Fixpoint.IndPredAndFn F p = F fun (x : α) => Fixpoint.IndPred F x ∧ p x

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

Equations

• Fixpoint.IndPredAnd F = Fixpoint.IndPred (Fixpoint.IndPredAndFn F)

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

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

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

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

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

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

theorem Fixpoint.indPredAnd_le_indPred {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : IndPredAnd F ≤ IndPred F

theorem Fixpoint.indPredAnd_eq_indPred {α : Type u_1} {F : (α → Prop) → α → Prop} (hf : Monotone F) : IndPredAnd F = IndPred F

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

theorem Fixpoint.eq_of_ctor_and_ind_eq_aux₁ {α : Type u_1} {F : (α → Prop) → α → Prop} {x : α} {p q : α → Prop} (hf : Monotone F) (h₁ : ∀ ⦃x : α⦄, F q x → q x) (h₂ : ∀ ⦃p₁ : α → Prop⦄ ⦃x : α⦄, p x → (∀ ⦃y : α⦄, F (fun (x : α) => p x ∧ p₁ x) y → p₁ y) → p₁ x) (h : p x) : q x

theorem Fixpoint.eq_of_ctor_and_ind_eq {α : Type u_1} {F : (α → Prop) → α → Prop} {p q : α → Prop} (hf : Monotone F) (h₁ : ∀ ⦃x : α⦄, F p x → p x) (h₂ : ∀ ⦃x : α⦄, F q x → q x) (h₃ : ∀ ⦃p₁ : α → Prop⦄ ⦃x : α⦄, p x → (∀ ⦃y : α⦄, F (fun (x : α) => p x ∧ p₁ x) y → p₁ y) → p₁ x) (h₄ : ∀ ⦃p₁ : α → Prop⦄ ⦃x : α⦄, q x → (∀ ⦃y : α⦄, F (fun (x : α) => q x ∧ p₁ x) y → p₁ y) → p₁ x) : p = q