This file contains convenience theorems around WellFoundedRelations. Right now, it only features minimal_elem_for_prop_exists that returns the minimal element of a WellFoundedRelation that fulfills a given property. This is basically the well-ordering principle.

theorem minimal_element_for_property_and_relation {α : Type u} [rel : WellFoundedRelation α] (prop : α → Prop) (a : α) (ha : prop a) : ∃ (a : α), prop a ∧ ∀ (b : α), WellFoundedRelation.rel b a → ¬prop b

If a there is an element such that a certain property holds, then there is a smallest such element.

theorem minimal_element_for_property_and_transitive_relation {α : Type u} [rel : WellFoundedRelation α] (trans : ∀ (a b c : α), WellFoundedRelation.rel a b → WellFoundedRelation.rel b c → WellFoundedRelation.rel a c) (prop : α → Prop) (a : α) (ha : prop a) : ∃ (c : α), prop c ∧ (c = a ∨ WellFoundedRelation.rel c a) ∧ ∀ (b : α), WellFoundedRelation.rel b c → ¬prop b

If a there is an element such that a certain property holds, then there is a smallest such element that is a predecessor of the original element.