Documentation

Mathlib.Logic.Pairwise

Relations holding pairwise #

This file defines pairwise relations.

Main declarations #

def Pairwise {α : Type u_1} (r : ααProp) :

A relation r holds pairwise if r i j for all i ≠ j.

Equations
Instances For
    theorem Pairwise.mono {α : Type u_1} {r : ααProp} {p : ααProp} (hr : Pairwise r) (h : ∀ ⦃i j : α⦄, r i jp i j) :
    theorem Pairwise.eq {α : Type u_1} {r : ααProp} {a : α} {b : α} (h : Pairwise r) :
    ¬r a ba = b
    theorem Subsingleton.pairwise {α : Type u_1} {r : ααProp} [Subsingleton α] :
    theorem Function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} :
    Function.Injective f Pairwise ((fun (x1 x2 : α) => x1 x2) on f)
    theorem Function.Injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} :
    Function.Injective fPairwise ((fun (x1 x2 : α) => x1 x2) on f)

    Alias of the forward direction of Function.injective_iff_pairwise_ne.

    theorem Pairwise.comp_of_injective {α : Type u_1} {β : Type u_2} {r : ααProp} (hr : Pairwise r) {f : βα} (hf : Function.Injective f) :
    Pairwise (r on f)
    theorem Pairwise.of_comp_of_surjective {α : Type u_1} {β : Type u_2} {r : ααProp} {f : βα} (hr : Pairwise (r on f)) (hf : Function.Surjective f) :
    theorem Function.Bijective.pairwise_comp_iff {α : Type u_1} {β : Type u_2} {r : ααProp} {f : βα} (hf : Function.Bijective f) :
    def Set.Pairwise {α : Type u_1} (s : Set α) (r : ααProp) :

    The relation r holds pairwise on the set s if r x y for all distinct x y ∈ s.

    Equations
    • s.Pairwise r = ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sx yr x y
    Instances For
      theorem Set.pairwise_of_forall {α : Type u_1} (s : Set α) (r : ααProp) (h : ∀ (a b : α), r a b) :
      s.Pairwise r
      theorem Set.Pairwise.imp_on {α : Type u_1} {r : ααProp} {p : ααProp} {s : Set α} (h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a bp a b) :
      s.Pairwise p
      theorem Set.Pairwise.imp {α : Type u_1} {r : ααProp} {p : ααProp} {s : Set α} (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a bp a b) :
      s.Pairwise p
      theorem Set.Pairwise.eq {α : Type u_1} {r : ααProp} {s : Set α} {a : α} {b : α} (hs : s.Pairwise r) (ha : a s) (hb : b s) (h : ¬r a b) :
      a = b
      theorem Reflexive.set_pairwise_iff {α : Type u_1} {r : ααProp} {s : Set α} (hr : Reflexive r) :
      s.Pairwise r ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr a b
      theorem Set.Pairwise.on_injective {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} {s : Set α} (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ (x : ι), f x s) :
      Pairwise (r on f)
      theorem Pairwise.set_pairwise {α : Type u_1} {r : ααProp} (h : Pairwise r) (s : Set α) :
      s.Pairwise r