Documentation

Mathlib.Logic.Relator

Relator for functions, pairs, sums, and lists. #

def Relator.LiftFun {α : Sort u₁} {β : Sort u₂} {γ : Sort v₁} {δ : Sort v₂} (R : αβProp) (S : γδProp) (f : αγ) (g : βδ) :

The binary relations R : α → β → Prop and S : γ → δ → Prop induce a binary relation on functions LiftFun : (α → γ) → (β → δ) → Prop.

Equations
  • (R S) f g = ∀ ⦃a : α⦄ ⦃b : β⦄, R a bS (f a) (g b)
Instances For

    (R ⇒ S) f g means LiftFun R S f g.

    Equations
    Instances For
      def Relator.RightTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

      A relation is "right total" if every element appears on the right.

      Equations
      Instances For
        def Relator.LeftTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

        A relation is "left total" if every element appears on the left.

        Equations
        Instances For
          def Relator.BiTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

          A relation is "bi-total" if it is both right total and left total.

          Equations
          Instances For
            def Relator.LeftUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

            A relation is "left unique" if every element on the right is paired with at most one element on the left.

            Equations
            Instances For
              def Relator.RightUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

              A relation is "right unique" if every element on the left is paired with at most one element on the right.

              Equations
              Instances For
                def Relator.BiUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

                A relation is "bi-unique" if it is both left unique and right unique.

                Equations
                Instances For
                  theorem Relator.RightTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.RightTotal R) :
                  ((R fun (x1 : Sort u_1) (x2 : Prop) => x1x2) fun (x1 : Sort (imax (u₁ + 1) u_1)) (x2 : Prop) => x1x2) (fun (p : αSort u_1) => (i : α) → p i) fun (q : βProp) => ∀ (i : β), q i
                  theorem Relator.LeftTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.LeftTotal R) :
                  ((R fun (x1 x2 : Prop) => x1x2) fun (x1 x2 : Prop) => x1x2) (fun (p : αProp) => ∃ (i : α), p i) fun (q : βProp) => ∃ (i : β), q i
                  theorem Relator.BiTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.BiTotal R) :
                  ((R Iff) Iff) (fun (p : αProp) => ∀ (i : α), p i) fun (q : βProp) => ∀ (i : β), q i
                  theorem Relator.BiTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.BiTotal R) :
                  ((R Iff) Iff) (fun (p : αProp) => ∃ (i : α), p i) fun (q : βProp) => ∃ (i : β), q i
                  theorem Relator.left_unique_of_rel_eq {α : Type u₁} {β : Type u₂} {R : αβProp} {eq' : ββProp} (he : (R R Iff) Eq eq') :
                  theorem Relator.rel_imp :
                  (Iff Iff Iff) (fun (x1 x2 : Prop) => x1x2) fun (x1 x2 : Prop) => x1x2
                  theorem Relator.LeftUnique.flip {α : Type u_1} {β : Type u_2} {r : αβProp} (h : Relator.LeftUnique r) :
                  theorem Relator.rel_and :
                  ((fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2
                  theorem Relator.rel_or :
                  ((fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2
                  theorem Relator.rel_iff :
                  ((fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : Prop) => x1 x2) fun (x1 x2 : Prop) => x1 x2
                  theorem Relator.rel_eq {α : Type u_1} {β : Type u_2} {r : αβProp} (hr : Relator.BiUnique r) :
                  (r r fun (x1 x2 : Prop) => x1 x2) (fun (x1 x2 : α) => x1 = x2) fun (x1 x2 : β) => x1 = x2
                  theorem Relator.LeftTotal.refl {α : Type u_5} {r₁₁ : ααProp} (hr : ∀ (a : α), r₁₁ a a) :
                  theorem Relator.LeftTotal.symm {β : Type u_2} {α : Type u_5} {r₁₂ : αβProp} {r₂₁ : βαProp} (hr : ∀ (a : α) (b : β), r₁₂ a br₂₁ b a) :
                  theorem Relator.LeftTotal.trans {β : Type u_2} {γ : Type u_3} {α : Type u_5} {r₁₂ : αβProp} {r₂₃ : βγProp} {r₁₃ : αγProp} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a br₂₃ b cr₁₃ a c) :
                  Relator.LeftTotal r₁₂Relator.LeftTotal r₂₃Relator.LeftTotal r₁₃
                  theorem Relator.RightTotal.refl {α : Type u_5} {r₁₁ : ααProp} (hr : ∀ (a : α), r₁₁ a a) :
                  theorem Relator.RightTotal.symm {β : Type u_2} {α : Type u_5} {r₁₂ : αβProp} {r₂₁ : βαProp} (hr : ∀ (a : α) (b : β), r₁₂ a br₂₁ b a) :
                  theorem Relator.RightTotal.trans {β : Type u_2} {γ : Type u_3} {α : Type u_5} {r₁₂ : αβProp} {r₂₃ : βγProp} {r₁₃ : αγProp} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a br₂₃ b cr₁₃ a c) :
                  theorem Relator.BiTotal.refl {α : Type u_5} {r₁₁ : ααProp} (hr : ∀ (a : α), r₁₁ a a) :
                  theorem Relator.BiTotal.symm {β : Type u_2} {α : Type u_5} {r₁₂ : αβProp} {r₂₁ : βαProp} (hr : ∀ (a : α) (b : β), r₁₂ a br₂₁ b a) :
                  Relator.BiTotal r₁₂Relator.BiTotal r₂₁
                  theorem Relator.BiTotal.trans {β : Type u_2} {γ : Type u_3} {α : Type u_5} {r₁₂ : αβProp} {r₂₃ : βγProp} {r₁₃ : αγProp} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a br₂₃ b cr₁₃ a c) :
                  Relator.BiTotal r₁₂Relator.BiTotal r₂₃Relator.BiTotal r₁₃