Documentation

Foundation.Vorspiel.Order

def IsInfiniteDescendingChain {α : Sort u} (r : ααProp) (c : α) :
Equations
Instances For
    noncomputable def descendingChain {α : Sort u} (r : ααProp) (z : α) :
    α
    Equations
    Instances For
      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 : α) :
      theorem isInfiniteDescendingChain_of_non_acc {α : Sort u} (r : ααProp) (z : α) (hz : ¬Acc 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