Documentation

Foundation.Vorspiel.BinaryRelations

def Euclidean {α : Type u} (rel : ααProp) :
Equations
  • Euclidean rel = ∀ ⦃x y z : α⦄, rel x yrel x zrel z y
Instances For
    def Serial {α : Type u} (rel : ααProp) :
    Equations
    • Serial rel = ∀ (x : α), ∃ (y : α), rel x y
    Instances For
      def Confluent {α : Type u} (rel : ααProp) :
      Equations
      • Confluent rel = ∀ ⦃x y z : α⦄, rel x y rel x z∃ (w : α), rel y w rel z w
      Instances For
        def Dense {α : Type u} (rel : ααProp) :
        Equations
        • Dense rel = ∀ ⦃x y : α⦄, rel x y∃ (z : α), rel x z rel z y
        Instances For
          def Connected {α : Type u} (rel : ααProp) :
          Equations
          • Connected rel = ∀ ⦃x y z : α⦄, rel x y rel x zrel y z rel z y
          Instances For
            def Functional {α : Type u} (rel : ααProp) :
            Equations
            Instances For
              def RightConvergent {α : Type u} (rel : ααProp) :
              Equations
              Instances For
                def Extensive {α : Type u} (rel : ααProp) :
                Equations
                Instances For
                  def Antisymmetric {α : Type u} (rel : ααProp) :
                  Equations
                  Instances For
                    def Isolated {α : Type u} (rel : ααProp) :
                    Equations
                    Instances For
                      def Assymetric {α : Type u} (rel : ααProp) :
                      Equations
                      Instances For
                        def Universal {α : Type u} (rel : ααProp) :
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev ConverseWellFounded {α : Type u} (rel : ααProp) :
                          Equations
                          Instances For
                            theorem serial_of_refl {α : Type u} {rel : ααProp} (hRefl : Reflexive rel) :
                            Serial rel
                            theorem eucl_of_symm_trans {α : Type u} {rel : ααProp} (hSymm : Symmetric rel) (hTrans : Transitive rel) :
                            theorem trans_of_symm_eucl {α : Type u} {rel : ααProp} (hSymm : Symmetric rel) (hEucl : Euclidean rel) :
                            theorem symm_of_refl_eucl {α : Type u} {rel : ααProp} (hRefl : Reflexive rel) (hEucl : Euclidean rel) :
                            theorem trans_of_refl_eucl {α : Type u} {rel : ααProp} (hRefl : Reflexive rel) (hEucl : Euclidean rel) :
                            theorem refl_of_symm_serial_eucl {α : Type u} {rel : ααProp} (hSymm : Symmetric rel) (hSerial : Serial rel) (hEucl : Euclidean rel) :
                            theorem ConverseWellFounded.iff_has_max {α : Type u} {r : ααProp} :
                            ConverseWellFounded r ∀ (s : Set α), s.Nonemptyms, xs, ¬r m x
                            theorem Finite.converseWellFounded_of_trans_irrefl {α : Type u} {rel : ααProp} [Finite α] [IsTrans α rel] [IsIrrefl α rel] :
                            theorem Finite.converseWellFounded_of_trans_irrefl' {α : Type u} {rel : ααProp} (hFinite : Finite α) (hTrans : Transitive rel) (hIrrefl : Irreflexive rel) :
                            theorem extensive_of_reflex_antisymm_eucl {α : Type u} {rel : ααProp} (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) :
                            theorem irreflexive_of_assymetric {α : Type u} {rel : ααProp} (hAssym : Assymetric rel) :
                            theorem refl_of_universal {α : Type u} {rel : ααProp} (h : Universal rel) :
                            theorem eucl_of_universal {α : Type u} {rel : ααProp} (h : Universal rel) :
                            @[simp]
                            theorem WellFounded.trivial_wellfounded {α : Type u} :
                            WellFounded fun (x x : α) => False
                            def Relation.IrreflGen {α : Type u} (R : ααProp) (x : α) (y : α) :
                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev WeaklyConverseWellFounded {α : Type u} (R : ααProp) :
                              Equations
                              Instances For
                                def WCWF {α : Type u} (R : ααProp) :

                                Alias of WeaklyConverseWellFounded.

                                Equations
                                Instances For
                                  theorem dependent_choice {α : Type u} {R : ααProp} (h : ∃ (s : Set α), s.Nonempty as, bs, R a b) :
                                  ∃ (f : α), ∀ (x : ), R (f x) (f (x + 1))
                                  theorem Finite.exists_ne_map_eq_of_infinite_lt {α : Type u_1} {β : Sort u_2} [LinearOrder α] [Infinite α] [Finite β] (f : αβ) :
                                  ∃ (x : α) (y : α), x < y f x = f y
                                  theorem antisymm_of_WCWF {α : Type u} {R : ααProp} :
                                  theorem WCWF_of_finite_trans_antisymm {α : Type u} {R : ααProp} (hFin : Finite α) (R_trans : Transitive R) :