Order

def IsInfiniteDescendingChain {α : Sort u} (r : α → α → Prop) (c : ℕ → α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• IsInfiniteDescendingChain r c = ∀ (i : ℕ), r (c (i + 1)) (c i)

noncomputable def descendingChain {α : Sort u} (r : α → α → Prop) (z : α) : ℕ → α

Imported declaration from the Incompleteness formalization.

Equations

• descendingChain r z 0 = z
• descendingChain r z i.succ = Classical.epsilon fun (y : α) => r y (descendingChain r z i) ∧ ¬Acc r y

theorem not_acc_iff {α : Sort u} (r : α → α → Prop) {x : α} : ¬Acc r x ↔ ∃ (y : α), r y x ∧ ¬Acc r y

@[simp]

theorem descending_chain_zero {α : Sort u} (r : α → α → Prop) (z : α) : descendingChain r z 0 = z

theorem isInfiniteDescendingChain_of_non_acc {α : Sort u} (r : α → α → Prop) (z : α) (hz : ¬Acc r z) : IsInfiniteDescendingChain r (descendingChain r z)

theorem himp_himp_inf_himp_inf_le {α : Type u_1} [HeytingAlgebra α] (a b c : α) : (a ⇨ b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c

theorem himp_inf_himp_inf_sup_le {α : Type u_1} [HeytingAlgebra α] (a b c : α) : (a ⇨ c) ⊓ (b ⇨ c) ⊓ (a ⊔ b) ≤ c